Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.41v GIF version

Theorem 19.41v 1782
 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
StepHypRef Expression
1 ax-17 1419 . 2 (𝜓 → ∀𝑥𝜓)
2119.41h 1575 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  19.41vv  1783  19.41vvv  1784  19.41vvvv  1785  eeeanv  1808  gencbvex  2600  euxfrdc  2727  euind  2728  r19.9rmv  3313  opabm  4017  eliunxp  4475  relop  4486  dmuni  4545  dmres  4632  dminss  4738  imainss  4739  ssrnres  4763  cnvresima  4810  resco  4825  rnco  4827  coass  4839  xpcom  4864  f11o  5159  fvelrnb  5221  rnoprab  5587  domen  6232  xpassen  6304  genpassl  6622  genpassu  6623
 Copyright terms: Public domain W3C validator