Theorem 19.42v 1921

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1924  19.42vv  1926  19.42vvv  1927  4exdistr  1931  cbvex2  1937  2sb5  2002  2sb5rf  2008  rexcom4a  2787  ceqsex2  2804  reuind  2969  2rmorex  2970  sbccomlem  3064  bm1.3ii  4154  opm  4267  eqvinop  4276  uniuni  4486  elco  4832  dmopabss  4878  dmopab3  4879  mptpreima  5163  brprcneu  5551  relelfvdm  5590  fndmin  5669  fliftf  5846  dfoprab2  5969  dmoprab  6003  dmoprabss  6004  fnoprabg  6023  opabex3d  6178  opabex3  6179  eroveu  6685  dmaddpq  7446  dmmulpq  7447  prarloc  7570  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  shftdm  10987  fngsum  13031  igsumvalx  13032  ntreq0  14368  bdbm1.3ii  15537