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

Theorem cbvralfw 3358
Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3361 with a disjoint variable condition, which does not require ax-10 2139, ax-13 2372. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 23-May-2024.)
Hypotheses
Ref Expression
cbvralfw.1 𝑥𝐴
cbvralfw.2 𝑦𝐴
cbvralfw.3 𝑦𝜑
cbvralfw.4 𝑥𝜓
cbvralfw.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralfw (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem cbvralfw
StepHypRef Expression
1 cbvralfw.2 . . . . 5 𝑦𝐴
21nfcri 2893 . . . 4 𝑦 𝑥𝐴
3 cbvralfw.3 . . . 4 𝑦𝜑
42, 3nfim 1900 . . 3 𝑦(𝑥𝐴𝜑)
5 cbvralfw.1 . . . . 5 𝑥𝐴
65nfcri 2893 . . . 4 𝑥 𝑦𝐴
7 cbvralfw.4 . . . 4 𝑥𝜓
86, 7nfim 1900 . . 3 𝑥(𝑦𝐴𝜓)
9 eleq1w 2821 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
10 cbvralfw.5 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
119, 10imbi12d 344 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
124, 8, 11cbvalv1 2340 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
13 df-ral 3068 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
14 df-ral 3068 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
1512, 13, 143bitr4i 302 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1537  wnf 1787  wcel 2108  wnfc 2886  wral 3063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-11 2156  ax-12 2173
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068
This theorem is referenced by:  cbvrexfw  3360  cbvralw  3363  reusv2lem4  5319  reusv2  5321  ffnfvf  6975  nnwof  12583  nnindf  31035  scottexf  36253  scott0f  36254  evth2f  42447  evthf  42459  supxrleubrnmptf  42881  stoweidlem14  43445  stoweidlem28  43459  stoweidlem59  43490
  Copyright terms: Public domain W3C validator