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

Theorem r19.42v 2663
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 2662 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 266 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 2513 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 266 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 212 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  wrex 2485
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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557
This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-rex 2490
This theorem is referenced by:  ceqsrexbv  2904  ceqsrex2v  2905  2reuswapdc  2977  iunrab  3975  iunin2  3991  iundif2ss  3993  iunopab  4328  elxp2  4693  cnvuni  4864  elunirn  5835  f1oiso  5895  oprabrexex2  6215  genpdflem  7620  1idprl  7703  1idpru  7704  ltexprlemm  7713  rexuz2  9702  4fvwrd4  10262  divalgb  12236
  Copyright terms: Public domain W3C validator