Theorem 19.42v 1931

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1934  19.42vv  1936  19.42vvv  1937  4exdistr  1941  cbvex2  1947  2sb5  2012  2sb5rf  2018  rexcom4a  2801  ceqsex2  2818  reuind  2985  2rmorex  2986  sbccomlem  3080  bm1.3ii  4181  opm  4296  eqvinop  4305  uniuni  4516  elco  4862  dmopabss  4909  dmopab3  4910  mptpreima  5195  brprcneu  5592  relelfvdm  5631  fndmin  5710  fliftf  5891  dfoprab2  6015  dmoprab  6049  dmoprabss  6050  fnoprabg  6069  opabex3d  6229  opabex3  6230  eroveu  6736  dmaddpq  7527  dmmulpq  7528  prarloc  7651  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  shftdm  11248  fngsum  13335  igsumvalx  13336  ntreq0  14719  bdbm1.3ii  16026