MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbidv2 Structured version   Visualization version   GIF version

Theorem rexbidv2 3173
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rexbidv2.1 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
Assertion
Ref Expression
rexbidv2 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem rexbidv2
StepHypRef Expression
1 rexbidv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
21exbidv 1919 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) ↔ ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3069 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3069 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wex 1776  wcel 2106  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-rex 3069
This theorem is referenced by:  rexbidva  3175  rexeqbidv  3345  rexss  4071  iuneq12d  5026  exopxfr2  5858  isoini  7358  rexsupp  8206  omabs  8688  elfi2  9452  wemapsolem  9588  ltexpi  10940  rexuz  12938  ncoprmgcdne1b  16684  lpigen  21363  llyi  23498  nllyi  23499  elpi1  25092  ressupprn  32705  xrecex  32887  bnj18eq1  34920  ldual1dim  39148  pmapjat1  39836  mrefg2  42695  islssfg2  43060  fourierdlem71  46133  hoiqssbl  46581  reuxfr1dd  48655  lubeldm2d  48755  glbeldm2d  48756
  Copyright terms: Public domain W3C validator