Theorem eqerlem 8490

Description: Lemma for eqer 8491. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)

Hypotheses

Ref	Expression
eqer.1	⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
eqer.2	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}

Assertion

Ref	Expression
eqerlem	⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)

Distinct variable groups:   𝑥,𝑤,𝑦   𝑥,𝑧,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝐴(𝑥,𝑧,𝑤)   𝐵(𝑦,𝑧,𝑤)   𝑅(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem eqerlem

Step	Hyp	Ref	Expression
1		eqer.2	. . 3 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}
2	1	brabsb 5437	. 2 ⊢ (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝐴 = 𝐵)
3		nfcsb1v 3853	. . . . 5 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐴
4		nfcsb1v 3853	. . . . 5 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐴
5	3, 4	nfeq 2919	. . . 4 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴
6		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑦 𝐴 = ⦋𝑤 / 𝑥⦌𝐴
7		vex 3426	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
8		eqer.1	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
9	7, 8	csbie 3864	. . . . . . . . 9 ⊢ ⦋𝑦 / 𝑥⦌𝐴 = 𝐵
10		csbeq1 3831	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
11	9, 10	eqtr3id 2793	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐴)
12	11	eqeq2d 2749	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (𝐴 = 𝐵 ↔ 𝐴 = ⦋𝑤 / 𝑥⦌𝐴))
13	6, 12	sbciegf 3750	. . . . . 6 ⊢ (𝑤 ∈ V → ([𝑤 / 𝑦]𝐴 = 𝐵 ↔ 𝐴 = ⦋𝑤 / 𝑥⦌𝐴))
14	13	elv 3428	. . . . 5 ⊢ ([𝑤 / 𝑦]𝐴 = 𝐵 ↔ 𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
15		csbeq1a 3842	. . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
16	15	eqeq1d 2740	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝐴 = ⦋𝑤 / 𝑥⦌𝐴 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴))
17	14, 16	syl5bb 282	. . . 4 ⊢ (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝐴 = 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴))
18	5, 17	sbciegf 3750	. . 3 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥][𝑤 / 𝑦]𝐴 = 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴))
19	18	elv 3428	. 2 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝐴 = 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
20	2, 19	bitri 274	1 ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  Vcvv 3422  [wsbc 3711  ⦋csb 3828   class class class wbr 5070  {copab 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133

This theorem is referenced by:  eqer  8491