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

Theorem r19.42v 2565
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 2564 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 264 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 2419 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 264 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 211 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wrex 2394
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-rex 2399
This theorem is referenced by:  ceqsrexbv  2790  ceqsrex2v  2791  2reuswapdc  2861  iunrab  3830  iunin2  3846  iundif2ss  3848  iunopab  4173  elxp2  4527  cnvuni  4695  elunirn  5635  f1oiso  5695  oprabrexex2  5996  genpdflem  7283  1idprl  7366  1idpru  7367  ltexprlemm  7376  rexuz2  9344  4fvwrd4  9885  divalgb  11549
  Copyright terms: Public domain W3C validator