Theorem cbvralfw 3304

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3348 with a disjoint variable condition, which does not require ax-10 2175, ax-13 2403. For a version not dependent on ax-11 2191 and ax-12, see cbvralvw 3242. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2175, ax-13 2403. (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 2916	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvralfw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfim 1925	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑)
5		cbvralfw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvralfw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfim 1925	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓)
9		eleq1w 2845	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvralfw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
12	4, 8, 11	cbvalv1 2372	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
13		df-ral 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
14		df-ral 3079	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
15	12, 13, 14	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567  Ⅎwnf 1812   ∈ wcel 2142  Ⅎwnfc 2909  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-11 2191  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-nf 1813  df-clel 2837  df-nfc 2911  df-ral 3079

This theorem is used by:  cbvrexfw  3305  cbvralw  3306  reusv2lem4  5371  reusv2  5373  ffnfvf  7115  nnwof  12944  nnindf  33175  scottexf  38845  scott0f  38846  rsp3  39043  evth2f  45763  evthf  45775  fmptff  46012  supxrleubrnmptf  46193  stoweidlem14  46756  stoweidlem28  46770  stoweidlem59  46801