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

Theorem cbvrex2v 3210
Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.)
Hypotheses
Ref Expression
cbvrex2v.1 (𝑥 = 𝑧 → (𝜑𝜒))
cbvrex2v.2 (𝑦 = 𝑤 → (𝜒𝜓))
Assertion
Ref Expression
cbvrex2v (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑧,𝐴   𝑤,𝐵   𝑥,𝐵,𝑦   𝑧,𝐵,𝑦   𝜒,𝑤   𝜒,𝑥   𝜑,𝑧   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤)   𝜓(𝑥,𝑧,𝑤)   𝜒(𝑦,𝑧)   𝐴(𝑦,𝑤)

Proof of Theorem cbvrex2v
StepHypRef Expression
1 cbvrex2v.1 . . . 4 (𝑥 = 𝑧 → (𝜑𝜒))
21rexbidv 3081 . . 3 (𝑥 = 𝑧 → (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜒))
32cbvrexv 3202 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑦𝐵 𝜒)
4 cbvrex2v.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvrexv 3202 . . 3 (∃𝑦𝐵 𝜒 ↔ ∃𝑤𝐵 𝜓)
65rexbii 3070 . 2 (∃𝑧𝐴𝑦𝐵 𝜒 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 264 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947
This theorem is referenced by:  omeu  7710  oeeui  7727  eroveu  7885  genpv  9859  bezoutlem3  15305  bezoutlem4  15306  bezout  15307  4sqlem2  15700  vdwnn  15749  efgrelexlema  18208  dyadmax  23412  2sqlem9  25197  2sq  25200  legov  25525  dfcgra2  25766  pstmfval  30067  nn0prpwlem  32442  isbnd2  33712  fourierdlem42  40684  fourierdlem54  40695  mogoldbb  41998
  Copyright terms: Public domain W3C validator