Theorem 19.42v 1958

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1961  19.42vv  1963  19.42vvv  1964  4exdistr  1968  cbvex2  1974  2sb5  2039  2sb5rf  2045  rexcom4a  2840  ceqsex2  2857  reuind  3025  2rmorex  3026  sbccomlem  3120  bm1.3ii  4237  opm  4356  eqvinop  4365  uniuni  4579  elco  4928  dmopabss  4975  dmopab3  4976  mptpreima  5263  brprcneu  5670  relelfvdm  5709  fndmin  5792  fliftf  5980  dfoprab2  6110  dmoprab  6144  dmoprabss  6145  fnoprabg  6164  opabex3d  6325  opabex3  6326  eroveu  6875  dmaddpq  7712  dmmulpq  7713  prarloc  7836  ltexprlemopl  7934  ltexprlemlol  7935  ltexprlemopu  7936  ltexprlemupu  7937  shftdm  11537  fngzsum  13657  gzsumvalx  13658  ntreq0  15128  bdbm1.3ii  16802