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

Theorem rexbidv2 3227
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 2017 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) ↔ ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3093 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3093 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 306 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  wex 1875  wcel 2157  wrex 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-ex 1876  df-rex 3093
This theorem is referenced by:  rexbidva  3228  rexss  3863  exopxfr2  5468  isoini  6814  rexsupp  7548  omabs  7965  elfi2  8560  wemapsolem  8695  ltexpi  10010  rexuz  11978  lpigen  19576  llyi  21603  nllyi  21604  elpi1  23169  xrecex  30136  bnj18eq1  31506  ldual1dim  35179  pmapjat1  35866  mrefg2  38044  islssfg2  38414  fourierdlem71  41125  hoiqssbl  41573
  Copyright terms: Public domain W3C validator