Theorem r19.2z 4518

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 3068	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1891	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4376	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3077	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ne 2947  df-ral 3068  df-rex 3077  df-dif 3979  df-nul 4353

This theorem is referenced by:  r19.2zb  4519  intssuni  4994  iinssiun  5028  riinn0  5106  iinexg  5366  reusv2lem2  5417  reusv2lem3  5418  xpiindi  5860  cnviin  6317  eusvobj2  7440  iiner  8847  finsschain  9429  cfeq0  10325  cfsuc  10326  iundom2g  10609  alephval2  10641  prlem934  11102  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  rexfiuz  15396  r19.2uz  15400  climuni  15598  caurcvg  15725  caurcvg2  15726  caucvg  15727  pc2dvds  16926  vdwmc2  17026  vdwlem6  17033  vdwnnlem3  17044  issubg4  19185  gexcl3  19629  lbsextlem2  21184  iincld  23068  opnnei  23149  cncnp2  23310  lmmo  23409  iunconn  23457  ptbasfi  23610  filuni  23914  isfcls  24038  fclsopn  24043  ustfilxp  24242  nrginvrcn  24734  lebnumlem3  25014  cfil3i  25322  caun0  25334  iscmet3  25346  nulmbl2  25590  dyadmax  25652  itg2seq  25797  itg2monolem1  25805  bddiblnc  25897  rolle  26048  c1lip1  26056  taylfval  26418  ulm0  26452  frgrreg  30426  bnj906  34906  cvmliftlem15  35266  dfon2lem6  35752  filnetlem4  36347  itg2addnclem  37631  itg2addnc  37634  itg2gt0cn  37635  ftc1anc  37661  filbcmb  37700  incsequz  37708  isbnd2  37743  isbnd3  37744  ssbnd  37748  unichnidl  37991  iunconnlem2  44906  upbdrech  45220  infxrpnf  45361