Theorem r19.2z 4060

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1892). 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	|- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem r19.2z

Step	Hyp	Ref	Expression
1		df-ral 2917	. . . 4 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		exintr 1819	. . . 4 |- ( A. x ( x e. A -> ph ) -> ( E. x x e. A -> E. x ( x e. A /\ ph ) ) )
3	1, 2	sylbi 207	. . 3 |- ( A. x e. A ph -> ( E. x x e. A -> E. x ( x e. A /\ ph ) ) )
4		n0 3931	. . 3 |- ( A =/= (/) <-> E. x x e. A )
5		df-rex 2918	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
6	3, 4, 5	3imtr4g 285	. 2 |- ( A. x e. A ph -> ( A =/= (/) -> E. x e. A ph ) )
7	6	impcom 446	1 |- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  r19.2zb  4061  intssuni  4499  riinn0  4595  trintssOLD  4770  iinexg  4824  reusv2lem2  4869  reusv2lem2OLD  4870  reusv2lem3  4871  xpiindi  5257  cnviin  5672  eusvobj2  6643  iiner  7819  finsschain  8273  cfeq0  9078  cfsuc  9079  iundom2g  9362  alephval2  9394  prlem934  9855  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  supmul  10995  rexfiuz  14087  r19.2uz  14091  climuni  14283  caurcvg  14407  caurcvg2  14408  caucvg  14409  pc2dvds  15583  vdwmc2  15683  vdwlem6  15690  vdwnnlem3  15701  issubg4  17613  gexcl3  18002  lbsextlem2  19159  iincld  20843  opnnei  20924  cncnp2  21085  lmmo  21184  iunconn  21231  ptbasfi  21384  filuni  21689  isfcls  21813  fclsopn  21818  ustfilxp  22016  nrginvrcn  22496  lebnumlem3  22762  cfil3i  23067  caun0  23079  iscmet3  23091  nulmbl2  23304  dyadmax  23366  itg2seq  23509  itg2monolem1  23517  rolle  23753  c1lip1  23760  taylfval  24113  ulm0  24145  frgrreg  27252  iinssiun  29377  bnj906  31000  cvmliftlem15  31280  dfon2lem6  31693  filnetlem4  32376  itg2addnclem  33461  itg2addnc  33464  itg2gt0cn  33465  bddiblnc  33480  ftc1anc  33493  filbcmb  33535  incsequz  33544  isbnd2  33582  isbnd3  33583  ssbnd  33587  unichnidl  33830  iunconnlem2  39171  upbdrech  39519  infxrpnf  39674