Theorem r19.2z 4093

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1949). 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 2946	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1859	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 207	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 3964	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 2947	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 285	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 445	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1521  ∃wex 1744   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-v 3233  df-dif 3610  df-nul 3949

This theorem is referenced by:  r19.2zb  4094  intssuni  4531  riinn0  4627  trintssOLD  4803  iinexg  4854  reusv2lem2  4899  reusv2lem2OLD  4900  reusv2lem3  4901  xpiindi  5290  cnviin  5710  eusvobj2  6683  iiner  7862  finsschain  8314  cfeq0  9116  cfsuc  9117  iundom2g  9400  alephval2  9432  prlem934  9893  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  supmul  11033  rexfiuz  14131  r19.2uz  14135  climuni  14327  caurcvg  14451  caurcvg2  14452  caucvg  14453  pc2dvds  15630  vdwmc2  15730  vdwlem6  15737  vdwnnlem3  15748  issubg4  17660  gexcl3  18048  lbsextlem2  19207  iincld  20891  opnnei  20972  cncnp2  21133  lmmo  21232  iunconn  21279  ptbasfi  21432  filuni  21736  isfcls  21860  fclsopn  21865  ustfilxp  22063  nrginvrcn  22543  lebnumlem3  22809  cfil3i  23113  caun0  23125  iscmet3  23137  nulmbl2  23350  dyadmax  23412  itg2seq  23554  itg2monolem1  23562  rolle  23798  c1lip1  23805  taylfval  24158  ulm0  24190  frgrreg  27381  iinssiun  29503  bnj906  31126  cvmliftlem15  31406  dfon2lem6  31817  filnetlem4  32501  itg2addnclem  33591  itg2addnc  33594  itg2gt0cn  33595  bddiblnc  33610  ftc1anc  33623  filbcmb  33665  incsequz  33674  isbnd2  33712  isbnd3  33713  ssbnd  33717  unichnidl  33960  iunconnlem2  39485  upbdrech  39833  infxrpnf  39987