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

Theorem r19.42v 2467
 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 2466 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 253 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 2331 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 253 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 201 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-rex 2312 This theorem is referenced by:  ceqsrexbv  2675  ceqsrex2v  2676  2reuswapdc  2743  iunrab  3704  iunin2  3720  iundif2ss  3722  iunopab  4018  elxp2  4363  cnvuni  4521  elunirn  5405  f1oiso  5465  oprabrexex2  5757  genpdflem  6605  1idprl  6688  1idpru  6689  ltexprlemm  6698  rexuz2  8524  4fvwrd4  8997
 Copyright terms: Public domain W3C validator