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

Theorem cbvrex2v 3393
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 3242 . . 3 (𝑥 = 𝑧 → (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜒))
32cbvrexv 3384 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑦𝐵 𝜒)
4 cbvrex2v.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvrexv 3384 . . 3 (∃𝑦𝐵 𝜒 ↔ ∃𝑤𝐵 𝜓)
65rexbii 3194 . 2 (∃𝑧𝐴𝑦𝐵 𝜒 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 267 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094
This theorem is referenced by:  omeu  8012  oeeui  8029  eroveu  8192  genpv  10219  bezoutlem3  15745  bezoutlem4  15746  bezout  15747  4sqlem2  16141  vdwnn  16190  efgrelexlema  18635  dyadmax  23902  2sqlem9  25705  2sq  25708  legov  26073  dfcgra2  26318  pstmfval  30786  fmla1  32203  nn0prpwlem  33197  isbnd2  34509  fourierdlem42  41871  fourierdlem54  41882  mogoldbb  43324
  Copyright terms: Public domain W3C validator