Theorem cbvralfw 3277

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3331 with a disjoint variable condition, which does not require ax-10 2147, ax-13 2377. For a version not dependent on ax-11 2163 and ax-12, see cbvralvw 3215. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2147, 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

Step	Hyp	Ref	Expression
1		cbvralfw.2	. . . . 5 ⊢ Ⅎ𝑦𝐴
2	1	nfcri 2891	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvralfw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfim 1898	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑)
5		cbvralfw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2891	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvralfw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfim 1898	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓)
9		eleq1w 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvralfw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
12	4, 8, 11	cbvalv1 2346	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
13		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
14		df-ral 3053	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
15	12, 13, 14	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884  ∀wral 3052

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 1969  ax-7 2010  ax-8 2116  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  cbvrexfw  3278  cbvralw  3279  reusv2lem4  5347  reusv2  5349  ffnfvf  7067  nnwof  12831  nnindf  32902  scottexf  38371  scott0f  38372  rsp3  38569  evth2f  45327  evthf  45339  fmptff  45580  supxrleubrnmptf  45762  stoweidlem14  46325  stoweidlem28  46339  stoweidlem59  46370