Theorem 19.42v 1918

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 1537	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	19.42h 1698	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1921  19.42vv  1923  19.42vvv  1924  4exdistr  1928  cbvex2  1934  2sb5  1995  2sb5rf  2001  rexcom4a  2776  ceqsex2  2792  reuind  2957  2rmorex  2958  sbccomlem  3052  bm1.3ii  4139  opm  4249  eqvinop  4258  uniuni  4466  elco  4808  dmopabss  4854  dmopab3  4855  mptpreima  5137  brprcneu  5523  relelfvdm  5562  fndmin  5639  fliftf  5816  dfoprab2  5938  dmoprab  5972  dmoprabss  5973  fnoprabg  5992  opabex3d  6140  opabex3  6141  eroveu  6644  dmaddpq  7396  dmmulpq  7397  prarloc  7520  ltexprlemopl  7618  ltexprlemlol  7619  ltexprlemopu  7620  ltexprlemupu  7621  shftdm  10849  ntreq0  14029  bdbm1.3ii  15040