Theorem r19.2z 4454

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 4312	. . 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 4292

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 3914  df-nul 4293

This theorem is referenced by:  r19.2zb  4455  intssuni  4930  iinssiun  4965  riinn0  5042  iinexg  5298  reusv2lem2  5349  reusv2lem3  5350  xpiindi  5789  cnviin  6247  eusvobj2  7361  iiner  8739  finsschain  9286  cfeq0  10185  cfsuc  10186  iundom2g  10469  alephval2  10501  prlem934  10962  supaddc  12126  supadd  12127  supmul1  12128  supmullem2  12130  supmul  12131  rexfiuz  15290  r19.2uz  15294  climuni  15494  caurcvg  15619  caurcvg2  15620  caucvg  15621  pc2dvds  16826  vdwmc2  16926  vdwlem6  16933  vdwnnlem3  16944  issubg4  19053  gexcl3  19493  lbsextlem2  21045  iincld  22902  opnnei  22983  cncnp2  23144  lmmo  23243  iunconn  23291  ptbasfi  23444  filuni  23748  isfcls  23872  fclsopn  23877  ustfilxp  24076  nrginvrcn  24556  lebnumlem3  24838  cfil3i  25145  caun0  25157  iscmet3  25169  nulmbl2  25413  dyadmax  25475  itg2seq  25619  itg2monolem1  25627  bddiblnc  25719  rolle  25870  c1lip1  25878  taylfval  26242  ulm0  26276  frgrreg  30296  bnj906  34893  cvmliftlem15  35258  dfon2lem6  35749  filnetlem4  36342  itg2addnclem  37638  itg2addnc  37641  itg2gt0cn  37642  ftc1anc  37668  filbcmb  37707  incsequz  37715  isbnd2  37750  isbnd3  37751  ssbnd  37755  unichnidl  37998  iunconnlem2  44897  upbdrech  45276  infxrpnf  45415  iuneqconst2  48784  iineqconst2  48785  iinxp  48792  iinfssc  49019