Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.2z | Structured version Visualization version GIF version |
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1892). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.) |
Ref | Expression |
---|---|
r19.2z | ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2917 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | exintr 1819 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 1, 2 | sylbi 207 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | n0 3931 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
5 | df-rex 2918 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | 3, 4, 5 | 3imtr4g 285 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑)) |
7 | 6 | impcom 446 | 1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∀wal 1481 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 ∅c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: r19.2zb 4061 intssuni 4499 riinn0 4595 trintssOLD 4770 iinexg 4824 reusv2lem2 4869 reusv2lem2OLD 4870 reusv2lem3 4871 xpiindi 5257 cnviin 5672 eusvobj2 6643 iiner 7819 finsschain 8273 cfeq0 9078 cfsuc 9079 iundom2g 9362 alephval2 9394 prlem934 9855 supaddc 10990 supadd 10991 supmul1 10992 supmullem2 10994 supmul 10995 rexfiuz 14087 r19.2uz 14091 climuni 14283 caurcvg 14407 caurcvg2 14408 caucvg 14409 pc2dvds 15583 vdwmc2 15683 vdwlem6 15690 vdwnnlem3 15701 issubg4 17613 gexcl3 18002 lbsextlem2 19159 iincld 20843 opnnei 20924 cncnp2 21085 lmmo 21184 iunconn 21231 ptbasfi 21384 filuni 21689 isfcls 21813 fclsopn 21818 ustfilxp 22016 nrginvrcn 22496 lebnumlem3 22762 cfil3i 23067 caun0 23079 iscmet3 23091 nulmbl2 23304 dyadmax 23366 itg2seq 23509 itg2monolem1 23517 rolle 23753 c1lip1 23760 taylfval 24113 ulm0 24145 frgrreg 27252 iinssiun 29377 bnj906 31000 cvmliftlem15 31280 dfon2lem6 31693 filnetlem4 32376 itg2addnclem 33461 itg2addnc 33464 itg2gt0cn 33465 bddiblnc 33480 ftc1anc 33493 filbcmb 33535 incsequz 33544 isbnd2 33582 isbnd3 33583 ssbnd 33587 unichnidl 33830 iunconnlem2 39171 upbdrech 39519 infxrpnf 39674 |
Copyright terms: Public domain | W3C validator |