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

Theorem cbvralfw 3304
Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3360 with a disjoint variable condition, which does not require ax-10 2141, ax-13 2377. For a version not dependent on ax-11 2157 and ax-12, see cbvralvw 3237. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2141, ax-13 2377. (Revised by GG, 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 2897 . . . 4 𝑦 𝑥𝐴
3 cbvralfw.3 . . . 4 𝑦𝜑
42, 3nfim 1896 . . 3 𝑦(𝑥𝐴𝜑)
5 cbvralfw.1 . . . . 5 𝑥𝐴
65nfcri 2897 . . . 4 𝑥 𝑦𝐴
7 cbvralfw.4 . . . 4 𝑥𝜓
86, 7nfim 1896 . . 3 𝑥(𝑦𝐴𝜓)
9 eleq1w 2824 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
10 cbvralfw.5 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
119, 10imbi12d 344 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
124, 8, 11cbvalv1 2343 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
13 df-ral 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
14 df-ral 3062 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
1512, 13, 143bitr4i 303 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wnf 1783  wcel 2108  wnfc 2890  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062
This theorem is referenced by:  cbvrexfw  3305  cbvralw  3306  reusv2lem4  5401  reusv2  5403  ffnfvf  7140  nnwof  12956  nnindf  32821  scottexf  38175  scott0f  38176  evth2f  45020  evthf  45032  fmptff  45276  supxrleubrnmptf  45462  stoweidlem14  46029  stoweidlem28  46043  stoweidlem59  46074
  Copyright terms: Public domain W3C validator