Theorem r19.2z 4495

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 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 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

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