MPE Home 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