Theorem 19.41v 1927

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistrv  1935  eeeanv  1962  gencbvex  2821  euxfrdc  2963  euind  2964  dfdif3  3287  r19.9rmv  3556  opabm  4334  eliunxp  4824  relop  4835  dmuni  4896  dmres  4988  dminss  5105  imainss  5106  ssrnres  5133  cnvresima  5180  resco  5195  rnco  5197  coass  5209  xpcom  5237  f11o  5566  fvelrnb  5638  rnoprab  6040  domen  6852  xpassen  6939  genpassl  7652  genpassu  7653