Theorem 19.41v 1874

Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.41v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.41h 1663	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistrv  1882  eeeanv  1905  gencbvex  2732  euxfrdc  2870  euind  2871  dfdif3  3186  r19.9rmv  3454  opabm  4202  eliunxp  4678  relop  4689  dmuni  4749  dmres  4840  dminss  4953  imainss  4954  ssrnres  4981  cnvresima  5028  resco  5043  rnco  5045  coass  5057  xpcom  5085  f11o  5400  fvelrnb  5469  rnoprab  5854  domen  6645  xpassen  6724  genpassl  7332  genpassu  7333