Theorem 19.42v 1841

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

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistr  1842  19.42vv  1843  19.42vvv  1844  4exdistr  1848  cbvex2  1852  2sb5  1914  2sb5rf  1920  rexcom4a  2657  ceqsex2  2673  reuind  2834  2rmorex  2835  sbccomlem  2927  bm1.3ii  3981  opm  4085  eqvinop  4094  uniuni  4301  elco  4633  dmopabss  4679  dmopab3  4680  mptpreima  4958  brprcneu  5333  relelfvdm  5371  fndmin  5445  fliftf  5616  dfoprab2  5734  dmoprab  5767  dmoprabss  5768  fnoprabg  5784  opabex3d  5930  opabex3  5931  eroveu  6423  dmaddpq  7035  dmmulpq  7036  prarloc  7159  ltexprlemopl  7257  ltexprlemlol  7258  ltexprlemopu  7259  ltexprlemupu  7260  shftdm  10371  ntreq0  11984  bdbm1.3ii  12499