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

Theorem rexbidv2 3077
Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 1890 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) ↔ ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 2947 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 2947 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 303 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wex 1744  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-rex 2947
This theorem is referenced by:  rexbidva  3078  rexss  3702  exopxfr2  5299  isoini  6628  rexsupp  7358  omabs  7772  elfi2  8361  wemapsolem  8496  ltexpi  9762  rexuz  11776  lpigen  19304  llyi  21325  nllyi  21326  elpi1  22891  xrecex  29756  bnj18eq1  31123  ldual1dim  34771  pmapjat1  35457  mrefg2  37587  islssfg2  37958  fourierdlem71  40712  hoiqssbl  41160
  Copyright terms: Public domain W3C validator