Theorem r19.2z 4454

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1978). 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 3053	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1894	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4307	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-ral 3053  df-rex 3063  df-dif 3906  df-nul 4288

This theorem is referenced by:  r19.2zb  4455  intssuni  4927  iinssiun  4962  riinn0  5040  iinexg  5295  reusv2lem2  5346  reusv2lem3  5347  xpiindi  5792  cnviin  6252  eusvobj2  7360  iiner  8738  finsschain  9271  cfeq0  10178  cfsuc  10179  iundom2g  10462  alephval2  10495  prlem934  10956  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  rexfiuz  15283  r19.2uz  15287  climuni  15487  caurcvg  15612  caurcvg2  15613  caucvg  15614  pc2dvds  16819  vdwmc2  16919  vdwlem6  16926  vdwnnlem3  16937  issubg4  19087  gexcl3  19528  lbsextlem2  21126  iincld  22995  opnnei  23076  cncnp2  23237  lmmo  23336  iunconn  23384  ptbasfi  23537  filuni  23841  isfcls  23965  fclsopn  23970  ustfilxp  24169  nrginvrcn  24648  lebnumlem3  24930  cfil3i  25237  caun0  25249  iscmet3  25261  nulmbl2  25505  dyadmax  25567  itg2seq  25711  itg2monolem1  25719  bddiblnc  25811  rolle  25962  c1lip1  25970  taylfval  26334  ulm0  26368  frgrreg  30481  bnj906  35106  cvmliftlem15  35514  dfon2lem6  36002  filnetlem4  36597  itg2addnclem  37922  itg2addnc  37925  itg2gt0cn  37926  ftc1anc  37952  filbcmb  37991  incsequz  37999  isbnd2  38034  isbnd3  38035  ssbnd  38039  unichnidl  38282  iunconnlem2  45290  upbdrech  45667  infxrpnf  45804  iuneqconst2  49182  iineqconst2  49183  iinxp  49190  iinfssc  49416