Theorem r19.2z 4446

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.)

Assertion

Ref	Expression
r19.2z	⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem r19.2z

Step	Hyp	Ref	Expression
1		df-ral 3045	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1892	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4304	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  ∅c0 4284

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ne 2926  df-ral 3045  df-rex 3054  df-dif 3906  df-nul 4285

This theorem is referenced by:  r19.2zb  4447  intssuni  4920  iinssiun  4955  riinn0  5032  iinexg  5287  reusv2lem2  5338  reusv2lem3  5339  xpiindi  5778  cnviin  6234  eusvobj2  7341  iiner  8716  finsschain  9249  cfeq0  10150  cfsuc  10151  iundom2g  10434  alephval2  10466  prlem934  10927  supaddc  12092  supadd  12093  supmul1  12094  supmullem2  12096  supmul  12097  rexfiuz  15255  r19.2uz  15259  climuni  15459  caurcvg  15584  caurcvg2  15585  caucvg  15586  pc2dvds  16791  vdwmc2  16891  vdwlem6  16898  vdwnnlem3  16909  issubg4  19024  gexcl3  19466  lbsextlem2  21066  iincld  22924  opnnei  23005  cncnp2  23166  lmmo  23265  iunconn  23313  ptbasfi  23466  filuni  23770  isfcls  23894  fclsopn  23899  ustfilxp  24098  nrginvrcn  24578  lebnumlem3  24860  cfil3i  25167  caun0  25179  iscmet3  25191  nulmbl2  25435  dyadmax  25497  itg2seq  25641  itg2monolem1  25649  bddiblnc  25741  rolle  25892  c1lip1  25900  taylfval  26264  ulm0  26298  frgrreg  30338  bnj906  34897  cvmliftlem15  35271  dfon2lem6  35762  filnetlem4  36355  itg2addnclem  37651  itg2addnc  37654  itg2gt0cn  37655  ftc1anc  37681  filbcmb  37720  incsequz  37728  isbnd2  37763  isbnd3  37764  ssbnd  37768  unichnidl  38011  iunconnlem2  44908  upbdrech  45287  infxrpnf  45425  iuneqconst2  48807  iineqconst2  48808  iinxp  48815  iinfssc  49042