Theorem 19.42v 1953

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1956  19.42vv  1958  19.42vvv  1959  4exdistr  1963  cbvex2  1969  2sb5  2034  2sb5rf  2040  rexcom4a  2824  ceqsex2  2841  reuind  3008  2rmorex  3009  sbccomlem  3103  bm1.3ii  4204  opm  4319  eqvinop  4328  uniuni  4541  elco  4887  dmopabss  4934  dmopab3  4935  mptpreima  5221  brprcneu  5619  relelfvdm  5658  fndmin  5741  fliftf  5922  dfoprab2  6050  dmoprab  6084  dmoprabss  6085  fnoprabg  6104  opabex3d  6264  opabex3  6265  eroveu  6771  dmaddpq  7562  dmmulpq  7563  prarloc  7686  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  shftdm  11328  fngsum  13416  igsumvalx  13417  ntreq0  14800  bdbm1.3ii  16212