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

Theorem r19.42v 2634
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 2633 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 266 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 2484 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 266 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 212 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  wrex 2456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-rex 2461
This theorem is referenced by:  ceqsrexbv  2868  ceqsrex2v  2869  2reuswapdc  2941  iunrab  3934  iunin2  3950  iundif2ss  3952  iunopab  4281  elxp2  4644  cnvuni  4813  elunirn  5766  f1oiso  5826  oprabrexex2  6130  genpdflem  7505  1idprl  7588  1idpru  7589  ltexprlemm  7598  rexuz2  9579  4fvwrd4  10137  divalgb  11924
  Copyright terms: Public domain W3C validator