| 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 1976). 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 3062 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 2 | exintr 1892 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
| 3 | 1, 2 | sylbi 217 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
| 4 | n0 4353 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
| 5 | df-rex 3071 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 6 | 3, 4, 5 | 3imtr4g 296 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑)) |
| 7 | 6 | impcom 407 | 1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1538 ∃wex 1779 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ne 2941 df-ral 3062 df-rex 3071 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: r19.2zb 4496 intssuni 4970 iinssiun 5005 riinn0 5083 iinexg 5348 reusv2lem2 5399 reusv2lem3 5400 xpiindi 5846 cnviin 6306 eusvobj2 7423 iiner 8829 finsschain 9399 cfeq0 10296 cfsuc 10297 iundom2g 10580 alephval2 10612 prlem934 11073 supaddc 12235 supadd 12236 supmul1 12237 supmullem2 12239 supmul 12240 rexfiuz 15386 r19.2uz 15390 climuni 15588 caurcvg 15713 caurcvg2 15714 caucvg 15715 pc2dvds 16917 vdwmc2 17017 vdwlem6 17024 vdwnnlem3 17035 issubg4 19163 gexcl3 19605 lbsextlem2 21161 iincld 23047 opnnei 23128 cncnp2 23289 lmmo 23388 iunconn 23436 ptbasfi 23589 filuni 23893 isfcls 24017 fclsopn 24022 ustfilxp 24221 nrginvrcn 24713 lebnumlem3 24995 cfil3i 25303 caun0 25315 iscmet3 25327 nulmbl2 25571 dyadmax 25633 itg2seq 25777 itg2monolem1 25785 bddiblnc 25877 rolle 26028 c1lip1 26036 taylfval 26400 ulm0 26434 frgrreg 30413 bnj906 34944 cvmliftlem15 35303 dfon2lem6 35789 filnetlem4 36382 itg2addnclem 37678 itg2addnc 37681 itg2gt0cn 37682 ftc1anc 37708 filbcmb 37747 incsequz 37755 isbnd2 37790 isbnd3 37791 ssbnd 37795 unichnidl 38038 iunconnlem2 44955 upbdrech 45317 infxrpnf 45457 |
| Copyright terms: Public domain | W3C validator |