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

Theorem rexxfr2d 5334
Description: Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
Hypotheses
Ref Expression
ralxfr2d.1 ((𝜑𝑦𝐶) → 𝐴𝑉)
ralxfr2d.2 (𝜑 → (𝑥𝐵 ↔ ∃𝑦𝐶 𝑥 = 𝐴))
ralxfr2d.3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexxfr2d (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑦𝐶 𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐶   𝜒,𝑥   𝜑,𝑥,𝑦   𝜓,𝑦
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)   𝐴(𝑦)   𝐶(𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem rexxfr2d
StepHypRef Expression
1 ralxfr2d.1 . . . 4 ((𝜑𝑦𝐶) → 𝐴𝑉)
2 ralxfr2d.2 . . . 4 (𝜑 → (𝑥𝐵 ↔ ∃𝑦𝐶 𝑥 = 𝐴))
3 ralxfr2d.3 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
43notbid 318 . . . 4 ((𝜑𝑥 = 𝐴) → (¬ 𝜓 ↔ ¬ 𝜒))
51, 2, 4ralxfr2d 5333 . . 3 (𝜑 → (∀𝑥𝐵 ¬ 𝜓 ↔ ∀𝑦𝐶 ¬ 𝜒))
65notbid 318 . 2 (𝜑 → (¬ ∀𝑥𝐵 ¬ 𝜓 ↔ ¬ ∀𝑦𝐶 ¬ 𝜒))
7 dfrex2 3170 . 2 (∃𝑥𝐵 𝜓 ↔ ¬ ∀𝑥𝐵 ¬ 𝜓)
8 dfrex2 3170 . 2 (∃𝑦𝐶 𝜒 ↔ ¬ ∀𝑦𝐶 ¬ 𝜒)
96, 7, 83bitr4g 314 1 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑦𝐶 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wral 3064  wrex 3065
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070
This theorem is referenced by:  rexrn  6963  rexima  7113  cnpresti  22439  cnprest  22440  1stcrest  22604  subislly  22632  txrest  22782  trfil2  23038  met1stc  23677  metucn  23727  xrlimcnp  26118  esumlub  32028  esumfsup  32038  ptrest  35776  djhcvat42  39429
  Copyright terms: Public domain W3C validator