Theorem 19.42v 1929

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

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1932  19.42vv  1934  19.42vvv  1935  4exdistr  1939  cbvex2  1945  2sb5  2010  2sb5rf  2016  rexcom4a  2795  ceqsex2  2812  reuind  2977  2rmorex  2978  sbccomlem  3072  bm1.3ii  4164  opm  4277  eqvinop  4286  uniuni  4497  elco  4843  dmopabss  4889  dmopab3  4890  mptpreima  5175  brprcneu  5568  relelfvdm  5607  fndmin  5686  fliftf  5867  dfoprab2  5991  dmoprab  6025  dmoprabss  6026  fnoprabg  6045  opabex3d  6205  opabex3  6206  eroveu  6712  dmaddpq  7491  dmmulpq  7492  prarloc  7615  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  shftdm  11104  fngsum  13191  igsumvalx  13192  ntreq0  14575  bdbm1.3ii  15789