Theorem 19.42v 1827

Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.42v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		ax-17 1459	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	19.42h 1617	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ∧ wa 102   ↔ wb 103  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  exdistr  1828  19.42vv  1829  19.42vvv  1830  4exdistr  1834  cbvex2  1838  2sb5  1900  2sb5rf  1906  rexcom4a  2623  ceqsex2  2639  reuind  2795  2rmorex  2796  sbccomlem  2888  bm1.3ii  3899  opm  3989  eqvinop  3998  uniuni  4201  dmopabss  4565  dmopab3  4566  mptpreima  4834  brprcneu  5191  relelfvdm  5226  fndmin  5295  fliftf  5459  dfoprab2  5572  dmoprab  5605  dmoprabss  5606  fnoprabg  5622  opabex3d  5768  opabex3  5769  eroveu  6220  dmaddpq  6569  dmmulpq  6570  prarloc  6693  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  shftdm  9710  bdbm1.3ii  10682