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  2784  euxfrdc  2924  euind  2925  dfdif3  3246  r19.9rmv  3515  opabm  4281  eliunxp  4767  relop  4778  dmuni  4838  dmres  4929  dminss  5044  imainss  5045  ssrnres  5072  cnvresima  5119  resco  5134  rnco  5136  coass  5148  xpcom  5176  f11o  5495  fvelrnb  5564  rnoprab  5958  domen  6751  xpassen  6830  genpassl  7523  genpassu  7524