Theorem 19.41v 1902

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1903  19.41vvv  1904  19.41vvvv  1905  exdistrv  1910  eeeanv  1933  gencbvex  2783  euxfrdc  2923  euind  2924  dfdif3  3245  r19.9rmv  3514  opabm  4278  eliunxp  4763  relop  4774  dmuni  4834  dmres  4925  dminss  5040  imainss  5041  ssrnres  5068  cnvresima  5115  resco  5130  rnco  5132  coass  5144  xpcom  5172  f11o  5491  fvelrnb  5560  rnoprab  5953  domen  6746  xpassen  6825  genpassl  7518  genpassu  7519