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

Theorem rexbidv2 3298
 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 1921 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) ↔ ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3147 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3147 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 316 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∃wex 1779   ∈ wcel 2113  ∃wrex 3142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910 This theorem depends on definitions:  df-bi 209  df-ex 1780  df-rex 3147 This theorem is referenced by:  rexbidva  3299  rexeqbidv  3405  rexss  4041  exopxfr2  5718  isoini  7094  rexsupp  7851  omabs  8277  elfi2  8881  wemapsolem  9017  ltexpi  10327  rexuz  12301  ncoprmgcdne1b  15997  lpigen  20032  llyi  22085  nllyi  22086  elpi1  23652  xrecex  30600  bnj18eq1  32203  ldual1dim  36306  pmapjat1  36993  mrefg2  39310  islssfg2  39677  fourierdlem71  42469  hoiqssbl  42914
 Copyright terms: Public domain W3C validator