![]() |
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 1981). 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 3066 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | exintr 1896 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 1, 2 | sylbi 216 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | n0 4307 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
5 | df-rex 3075 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | 3, 4, 5 | 3imtr4g 296 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑)) |
7 | 6 | impcom 409 | 1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∀wal 1540 ∃wex 1782 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 ∃wrex 3074 ∅c0 4283 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-ne 2945 df-ral 3066 df-rex 3075 df-dif 3914 df-nul 4284 |
This theorem is referenced by: r19.2zb 4454 intssuni 4932 iinssiun 4968 riinn0 5044 iinexg 5299 reusv2lem2 5355 reusv2lem3 5356 xpiindi 5792 cnviin 6239 eusvobj2 7350 iiner 8729 finsschain 9304 cfeq0 10193 cfsuc 10194 iundom2g 10477 alephval2 10509 prlem934 10970 supaddc 12123 supadd 12124 supmul1 12125 supmullem2 12127 supmul 12128 rexfiuz 15233 r19.2uz 15237 climuni 15435 caurcvg 15562 caurcvg2 15563 caucvg 15564 pc2dvds 16752 vdwmc2 16852 vdwlem6 16859 vdwnnlem3 16870 issubg4 18948 gexcl3 19370 lbsextlem2 20623 iincld 22393 opnnei 22474 cncnp2 22635 lmmo 22734 iunconn 22782 ptbasfi 22935 filuni 23239 isfcls 23363 fclsopn 23368 ustfilxp 23567 nrginvrcn 24059 lebnumlem3 24329 cfil3i 24636 caun0 24648 iscmet3 24660 nulmbl2 24903 dyadmax 24965 itg2seq 25110 itg2monolem1 25118 bddiblnc 25209 rolle 25357 c1lip1 25364 taylfval 25721 ulm0 25753 frgrreg 29341 bnj906 33545 cvmliftlem15 33895 dfon2lem6 34366 filnetlem4 34856 itg2addnclem 36132 itg2addnc 36135 itg2gt0cn 36136 ftc1anc 36162 filbcmb 36202 incsequz 36210 isbnd2 36245 isbnd3 36246 ssbnd 36250 unichnidl 36493 iunconnlem2 43224 upbdrech 43546 infxrpnf 43688 |
Copyright terms: Public domain | W3C validator |