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 1972). 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 3140 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | exintr 1884 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 1, 2 | sylbi 218 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | n0 4307 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
5 | df-rex 3141 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | 3, 4, 5 | 3imtr4g 297 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑)) |
7 | 6 | impcom 408 | 1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∀wal 1526 ∃wex 1771 ∈ wcel 2105 ≠ wne 3013 ∀wral 3135 ∃wrex 3136 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-dif 3936 df-nul 4289 |
This theorem is referenced by: r19.2zb 4437 intssuni 4889 iinssiun 4923 riinn0 4996 iinexg 5235 reusv2lem2 5290 reusv2lem3 5291 xpiindi 5699 cnviin 6130 eusvobj2 7138 iiner 8358 finsschain 8819 cfeq0 9666 cfsuc 9667 iundom2g 9950 alephval2 9982 prlem934 10443 supaddc 11596 supadd 11597 supmul1 11598 supmullem2 11600 supmul 11601 rexfiuz 14695 r19.2uz 14699 climuni 14897 caurcvg 15021 caurcvg2 15022 caucvg 15023 pc2dvds 16203 vdwmc2 16303 vdwlem6 16310 vdwnnlem3 16321 issubg4 18236 gexcl3 18641 lbsextlem2 19860 iincld 21575 opnnei 21656 cncnp2 21817 lmmo 21916 iunconn 21964 ptbasfi 22117 filuni 22421 isfcls 22545 fclsopn 22550 ustfilxp 22748 nrginvrcn 23228 lebnumlem3 23494 cfil3i 23799 caun0 23811 iscmet3 23823 nulmbl2 24064 dyadmax 24126 itg2seq 24270 itg2monolem1 24278 rolle 24514 c1lip1 24521 taylfval 24874 ulm0 24906 frgrreg 28100 bnj906 32101 cvmliftlem15 32442 dfon2lem6 32930 filnetlem4 33626 itg2addnclem 34824 itg2addnc 34827 itg2gt0cn 34828 bddiblnc 34843 ftc1anc 34856 filbcmb 34896 incsequz 34904 isbnd2 34942 isbnd3 34943 ssbnd 34947 unichnidl 35190 iunconnlem2 41146 upbdrech 41448 infxrpnf 41597 |
Copyright terms: Public domain | W3C validator |