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

Theorem 19.41v 1875
 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 1507 . 2 (𝜓 → ∀𝑥𝜓)
2119.41h 1664 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistrv  1883  eeeanv  1906  gencbvex  2735  euxfrdc  2873  euind  2874  dfdif3  3190  r19.9rmv  3458  opabm  4209  eliunxp  4685  relop  4696  dmuni  4756  dmres  4847  dminss  4960  imainss  4961  ssrnres  4988  cnvresima  5035  resco  5050  rnco  5052  coass  5064  xpcom  5092  f11o  5407  fvelrnb  5476  rnoprab  5861  domen  6652  xpassen  6731  genpassl  7355  genpassu  7356
 Copyright terms: Public domain W3C validator