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

Theorem cbvralfw 3420
 Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3423 with a disjoint variable condition, which does not require ax-10 2146, ax-13 2392. (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 2971 . . . 4 𝑦 𝑥𝐴
3 cbvralfw.3 . . . 4 𝑦𝜑
42, 3nfim 1898 . . 3 𝑦(𝑥𝐴𝜑)
5 cbvralfw.1 . . . . 5 𝑥𝐴
65nfcri 2971 . . . 4 𝑥 𝑦𝐴
7 cbvralfw.4 . . . 4 𝑥𝜓
86, 7nfim 1898 . . 3 𝑥(𝑦𝐴𝜓)
9 eleq1w 2898 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
10 cbvralfw.5 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
119, 10imbi12d 348 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
124, 8, 11cbvalv1 2363 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
13 df-ral 3137 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
14 df-ral 3137 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
1512, 13, 143bitr4i 306 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785   ∈ wcel 2115  Ⅎwnfc 2962  ∀wral 3132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-clel 2896  df-nfc 2964  df-ral 3137 This theorem is referenced by:  cbvrexfw  3422  cbvralw  3425  reusv2lem4  5283  reusv2  5285  ffnfvf  6864  nnwof  12300  nnindf  30532  scottexf  35506  scott0f  35507  evth2f  41480  evthf  41492  supxrleubrnmptf  41932  stoweidlem14  42498  stoweidlem28  42512  stoweidlem59  42543
 Copyright terms: Public domain W3C validator