Theorem cbvralfw 3368

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3371 with a disjoint variable condition, which does not require ax-10 2137, 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

Step	Hyp	Ref	Expression
1		cbvralfw.2	. . . . 5 ⊢ Ⅎ𝑦𝐴
2	1	nfcri 2894	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvralfw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfim 1899	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑)
5		cbvralfw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2894	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvralfw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfim 1899	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓)
9		eleq1w 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvralfw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	imbi12d 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
12	4, 8, 11	cbvalv1 2338	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
13		df-ral 3069	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
14		df-ral 3069	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
15	12, 13, 14	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-clel 2816  df-nfc 2889  df-ral 3069

This theorem is referenced by:  cbvrexfw  3370  cbvralw  3373  reusv2lem4  5324  reusv2  5326  ffnfvf  6993  nnwof  12654  nnindf  31133  scottexf  36326  scott0f  36327  evth2f  42558  evthf  42570  supxrleubrnmptf  42991  stoweidlem14  43555  stoweidlem28  43569  stoweidlem59  43600