Theorem 19.42v 1878

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistr  1881  19.42vv  1883  19.42vvv  1884  4exdistr  1888  cbvex2  1892  2sb5  1956  2sb5rf  1962  rexcom4a  2705  ceqsex2  2721  reuind  2884  2rmorex  2885  sbccomlem  2978  bm1.3ii  4044  opm  4151  eqvinop  4160  uniuni  4367  elco  4700  dmopabss  4746  dmopab3  4747  mptpreima  5027  brprcneu  5407  relelfvdm  5446  fndmin  5520  fliftf  5693  dfoprab2  5811  dmoprab  5845  dmoprabss  5846  fnoprabg  5865  opabex3d  6012  opabex3  6013  eroveu  6513  dmaddpq  7180  dmmulpq  7181  prarloc  7304  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  shftdm  10587  ntreq0  12290  bdbm1.3ii  13078