Theorem 19.41v 1889

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

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

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.41vv  1890  19.41vvv  1891  19.41vvvv  1892  exdistrv  1897  eeeanv  1920  gencbvex  2767  euxfrdc  2907  euind  2908  dfdif3  3227  r19.9rmv  3495  opabm  4252  eliunxp  4737  relop  4748  dmuni  4808  dmres  4899  dminss  5012  imainss  5013  ssrnres  5040  cnvresima  5087  resco  5102  rnco  5104  coass  5116  xpcom  5144  f11o  5459  fvelrnb  5528  rnoprab  5916  domen  6708  xpassen  6787  genpassl  7456  genpassu  7457