Theorem 19.42v 1956

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  1959  19.42vv  1961  19.42vvv  1962  4exdistr  1966  cbvex2  1972  2sb5  2037  2sb5rf  2043  rexcom4a  2838  ceqsex2  2855  reuind  3022  2rmorex  3023  sbccomlem  3117  bm1.3ii  4231  opm  4350  eqvinop  4359  uniuni  4572  elco  4921  dmopabss  4968  dmopab3  4969  mptpreima  5256  brprcneu  5663  relelfvdm  5702  fndmin  5785  fliftf  5972  dfoprab2  6100  dmoprab  6134  dmoprabss  6135  fnoprabg  6154  opabex3d  6314  opabex3  6315  eroveu  6860  dmaddpq  7694  dmmulpq  7695  prarloc  7818  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  shftdm  11507  fngsum  13601  igsumvalx  13602  ntreq0  14997  bdbm1.3ii  16661