Theorem 19.41v 1914

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  eeeanv  1949  gencbvex  2806  euxfrdc  2946  euind  2947  dfdif3  3269  r19.9rmv  3538  opabm  4311  eliunxp  4801  relop  4812  dmuni  4872  dmres  4963  dminss  5080  imainss  5081  ssrnres  5108  cnvresima  5155  resco  5170  rnco  5172  coass  5184  xpcom  5212  f11o  5533  fvelrnb  5604  rnoprab  6001  domen  6805  xpassen  6884  genpassl  7584  genpassu  7585