Theorem cbvralfw 3382

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3385 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (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 2943	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvralfw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfim 1897	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑)
5		cbvralfw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2943	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvralfw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfim 1897	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓)
9		eleq1w 2872	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvralfw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	imbi12d 348	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
12	4, 8, 11	cbvalv1 2350	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
13		df-ral 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
14		df-ral 3111	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
15	12, 13, 14	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-clel 2870  df-nfc 2938  df-ral 3111

This theorem is referenced by:  cbvrexfw  3384  cbvralw  3387  reusv2lem4  5267  reusv2  5269  ffnfvf  6860  nnwof  12302  nnindf  30561  scottexf  35606  scott0f  35607  evth2f  41644  evthf  41656  supxrleubrnmptf  42090  stoweidlem14  42656  stoweidlem28  42670  stoweidlem59  42701