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

Theorem rexbidv2 3175
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 1925 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) ↔ ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3072 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3072 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wex 1782  wcel 2107  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3072
This theorem is referenced by:  rexbidva  3177  rexeqbidv  3344  rexss  4056  exopxfr2  5845  isoini  7335  rexsupp  8167  omabs  8650  elfi2  9409  wemapsolem  9545  ltexpi  10897  rexuz  12882  ncoprmgcdne1b  16587  lpigen  20894  llyi  22978  nllyi  22979  elpi1  24561  ressupprn  31912  xrecex  32086  bnj18eq1  33938  ldual1dim  38036  pmapjat1  38724  mrefg2  41445  islssfg2  41813  fourierdlem71  44893  hoiqssbl  45341  lubeldm2d  47591  glbeldm2d  47592
  Copyright terms: Public domain W3C validator