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

Theorem r19.42v 2588
 Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 2587 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 264 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 2442 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 264 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 211 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wrex 2417 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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-rex 2422 This theorem is referenced by:  ceqsrexbv  2816  ceqsrex2v  2817  2reuswapdc  2888  iunrab  3860  iunin2  3876  iundif2ss  3878  iunopab  4203  elxp2  4557  cnvuni  4725  elunirn  5667  f1oiso  5727  oprabrexex2  6028  genpdflem  7329  1idprl  7412  1idpru  7413  ltexprlemm  7422  rexuz2  9390  4fvwrd4  9931  divalgb  11635
 Copyright terms: Public domain W3C validator