Theorem r19.2z 4425

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1980). 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 3069	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1895	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 216	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4280	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3070	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 408	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1537  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∅c0 4256

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ne 2944  df-ral 3069  df-rex 3070  df-dif 3890  df-nul 4257

This theorem is referenced by:  r19.2zb  4426  intssuni  4901  iinssiun  4937  riinn0  5012  iinexg  5265  reusv2lem2  5322  reusv2lem3  5323  xpiindi  5744  cnviin  6189  eusvobj2  7268  iiner  8578  finsschain  9126  cfeq0  10012  cfsuc  10013  iundom2g  10296  alephval2  10328  prlem934  10789  supaddc  11942  supadd  11943  supmul1  11944  supmullem2  11946  supmul  11947  rexfiuz  15059  r19.2uz  15063  climuni  15261  caurcvg  15388  caurcvg2  15389  caucvg  15390  pc2dvds  16580  vdwmc2  16680  vdwlem6  16687  vdwnnlem3  16698  issubg4  18774  gexcl3  19192  lbsextlem2  20421  iincld  22190  opnnei  22271  cncnp2  22432  lmmo  22531  iunconn  22579  ptbasfi  22732  filuni  23036  isfcls  23160  fclsopn  23165  ustfilxp  23364  nrginvrcn  23856  lebnumlem3  24126  cfil3i  24433  caun0  24445  iscmet3  24457  nulmbl2  24700  dyadmax  24762  itg2seq  24907  itg2monolem1  24915  bddiblnc  25006  rolle  25154  c1lip1  25161  taylfval  25518  ulm0  25550  frgrreg  28758  bnj906  32910  cvmliftlem15  33260  dfon2lem6  33764  filnetlem4  34570  itg2addnclem  35828  itg2addnc  35831  itg2gt0cn  35832  ftc1anc  35858  filbcmb  35898  incsequz  35906  isbnd2  35941  isbnd3  35942  ssbnd  35946  unichnidl  36189  iunconnlem2  42555  upbdrech  42844  infxrpnf  42986