Theorem 19.42v 1930

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1933  19.42vv  1935  19.42vvv  1936  4exdistr  1940  cbvex2  1946  2sb5  2011  2sb5rf  2017  rexcom4a  2796  ceqsex2  2813  reuind  2978  2rmorex  2979  sbccomlem  3073  bm1.3ii  4165  opm  4278  eqvinop  4287  uniuni  4498  elco  4844  dmopabss  4890  dmopab3  4891  mptpreima  5176  brprcneu  5569  relelfvdm  5608  fndmin  5687  fliftf  5868  dfoprab2  5992  dmoprab  6026  dmoprabss  6027  fnoprabg  6046  opabex3d  6206  opabex3  6207  eroveu  6713  dmaddpq  7492  dmmulpq  7493  prarloc  7616  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  shftdm  11133  fngsum  13220  igsumvalx  13221  ntreq0  14604  bdbm1.3ii  15827