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

Theorem 19.41v 1841
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 1474 . 2 (𝜓 → ∀𝑥𝜓)
2119.41h 1631 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wex 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.41vv  1842  19.41vvv  1843  19.41vvvv  1844  exdistrv  1847  eeeanv  1868  gencbvex  2687  euxfrdc  2823  euind  2824  dfdif3  3133  r19.9rmv  3401  opabm  4140  eliunxp  4616  relop  4627  dmuni  4687  dmres  4776  dminss  4889  imainss  4890  ssrnres  4917  cnvresima  4964  resco  4979  rnco  4981  coass  4993  xpcom  5021  f11o  5334  fvelrnb  5401  rnoprab  5786  domen  6575  xpassen  6653  genpassl  7233  genpassu  7234
  Copyright terms: Public domain W3C validator