Theorem r19.2z 4494

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1780   ∈ wcel 2105   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-ne 2940  df-ral 3061  df-rex 3070  df-dif 3951  df-nul 4323

This theorem is referenced by:  r19.2zb  4495  intssuni  4974  iinssiun  5010  riinn0  5086  iinexg  5341  reusv2lem2  5397  reusv2lem3  5398  xpiindi  5835  cnviin  6285  eusvobj2  7404  iiner  8789  finsschain  9365  cfeq0  10257  cfsuc  10258  iundom2g  10541  alephval2  10573  prlem934  11034  supaddc  12188  supadd  12189  supmul1  12190  supmullem2  12192  supmul  12193  rexfiuz  15301  r19.2uz  15305  climuni  15503  caurcvg  15630  caurcvg2  15631  caucvg  15632  pc2dvds  16819  vdwmc2  16919  vdwlem6  16926  vdwnnlem3  16937  issubg4  19068  gexcl3  19503  lbsextlem2  21006  iincld  22863  opnnei  22944  cncnp2  23105  lmmo  23204  iunconn  23252  ptbasfi  23405  filuni  23709  isfcls  23833  fclsopn  23838  ustfilxp  24037  nrginvrcn  24529  lebnumlem3  24809  cfil3i  25117  caun0  25129  iscmet3  25141  nulmbl2  25385  dyadmax  25447  itg2seq  25592  itg2monolem1  25600  bddiblnc  25691  rolle  25842  c1lip1  25850  taylfval  26210  ulm0  26242  frgrreg  30080  bnj906  34405  cvmliftlem15  34753  dfon2lem6  35230  filnetlem4  35730  itg2addnclem  37003  itg2addnc  37006  itg2gt0cn  37007  ftc1anc  37033  filbcmb  37072  incsequz  37080  isbnd2  37115  isbnd3  37116  ssbnd  37120  unichnidl  37363  iunconnlem2  44159  upbdrech  44474  infxrpnf  44615