Theorem 19.42v 1955

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1958  19.42vv  1960  19.42vvv  1961  4exdistr  1965  cbvex2  1971  2sb5  2036  2sb5rf  2042  rexcom4a  2827  ceqsex2  2844  reuind  3011  2rmorex  3012  sbccomlem  3106  bm1.3ii  4210  opm  4326  eqvinop  4335  uniuni  4548  elco  4896  dmopabss  4943  dmopab3  4944  mptpreima  5230  brprcneu  5632  relelfvdm  5671  fndmin  5754  fliftf  5939  dfoprab2  6067  dmoprab  6101  dmoprabss  6102  fnoprabg  6121  opabex3d  6282  opabex3  6283  eroveu  6794  dmaddpq  7598  dmmulpq  7599  prarloc  7722  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  shftdm  11382  fngsum  13470  igsumvalx  13471  ntreq0  14855  bdbm1.3ii  16486