Theorem 19.41v 1890

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 1514	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.41h 1673	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.41vv  1891  19.41vvv  1892  19.41vvvv  1893  exdistrv  1898  eeeanv  1921  gencbvex  2772  euxfrdc  2912  euind  2913  dfdif3  3232  r19.9rmv  3500  opabm  4258  eliunxp  4743  relop  4754  dmuni  4814  dmres  4905  dminss  5018  imainss  5019  ssrnres  5046  cnvresima  5093  resco  5108  rnco  5110  coass  5122  xpcom  5150  f11o  5465  fvelrnb  5534  rnoprab  5925  domen  6717  xpassen  6796  genpassl  7465  genpassu  7466