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

Theorem 19.41v 1798
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 1435 . 2 (𝜓 → ∀𝑥𝜓)
2119.41h 1591 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  19.41vv  1799  19.41vvv  1800  19.41vvvv  1801  eeeanv  1824  gencbvex  2617  euxfrdc  2750  euind  2751  r19.9rmv  3341  opabm  4045  eliunxp  4503  relop  4514  dmuni  4573  dmres  4660  dminss  4766  imainss  4767  ssrnres  4791  cnvresima  4838  resco  4853  rnco  4855  coass  4867  xpcom  4892  f11o  5187  fvelrnb  5249  rnoprab  5615  domen  6263  xpassen  6335  genpassl  6680  genpassu  6681
  Copyright terms: Public domain W3C validator