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  2825  ceqsex2  2842  reuind  3009  2rmorex  3010  sbccomlem  3104  bm1.3ii  4208  opm  4324  eqvinop  4333  uniuni  4546  elco  4894  dmopabss  4941  dmopab3  4942  mptpreima  5228  brprcneu  5628  relelfvdm  5667  fndmin  5750  fliftf  5935  dfoprab2  6063  dmoprab  6097  dmoprabss  6098  fnoprabg  6117  opabex3d  6278  opabex3  6279  eroveu  6790  dmaddpq  7589  dmmulpq  7590  prarloc  7713  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  shftdm  11373  fngsum  13461  igsumvalx  13462  ntreq0  14846  bdbm1.3ii  16422