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  4205  opm  4320  eqvinop  4329  uniuni  4542  elco  4888  dmopabss  4935  dmopab3  4936  mptpreima  5222  brprcneu  5622  relelfvdm  5661  fndmin  5744  fliftf  5929  dfoprab2  6057  dmoprab  6091  dmoprabss  6092  fnoprabg  6111  opabex3d  6272  opabex3  6273  eroveu  6781  dmaddpq  7577  dmmulpq  7578  prarloc  7701  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  shftdm  11348  fngsum  13436  igsumvalx  13437  ntreq0  14821  bdbm1.3ii  16309