Theorem eqsbc2VD

Description: Virtual deduction proof of eqsbc2 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	eqsbc2VD	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ 𝐶 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		idn1	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
2		eqsbc1	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ↔ 𝐴 = 𝐶 ) )
3	1 2	e1a	⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ↔ 𝐴 = 𝐶 )    )
4		eqcom	⊢ ( 𝐶 = 𝑥 ↔ 𝑥 = 𝐶 )
5	4	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 )
6	5	a1i	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ) )
7	1 6	e1a	⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 )    )
8		idn2	⊢ (    𝐴 ∈ 𝐵    ,    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    ▶    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    )
9		biimp	⊢ ( ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ) )
10	7 8 9	e12	⊢ (    𝐴 ∈ 𝐵    ,    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    ▶    [ 𝐴 / 𝑥 ] 𝑥 = 𝐶    )
11		biimp	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ↔ 𝐴 = 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 → 𝐴 = 𝐶 ) )
12	3 10 11	e12	⊢ (    𝐴 ∈ 𝐵    ,    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    ▶    𝐴 = 𝐶    )
13		eqcom	⊢ ( 𝐴 = 𝐶 ↔ 𝐶 = 𝐴 )
14	12 13	e2bi	⊢ (    𝐴 ∈ 𝐵    ,    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    ▶    𝐶 = 𝐴    )
15	14	in2	⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 → 𝐶 = 𝐴 )    )
16		idn2	⊢ (    𝐴 ∈ 𝐵    ,    𝐶 = 𝐴    ▶    𝐶 = 𝐴    )
17	16 13	e2bir	⊢ (    𝐴 ∈ 𝐵    ,    𝐶 = 𝐴    ▶    𝐴 = 𝐶    )
18		biimpr	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ↔ 𝐴 = 𝐶 ) → ( 𝐴 = 𝐶 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ) )
19	3 17 18	e12	⊢ (    𝐴 ∈ 𝐵    ,    𝐶 = 𝐴    ▶    [ 𝐴 / 𝑥 ] 𝑥 = 𝐶    )
20		biimpr	⊢ ( ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐶 → [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ) )
21	7 19 20	e12	⊢ (    𝐴 ∈ 𝐵    ,    𝐶 = 𝐴    ▶    [ 𝐴 / 𝑥 ] 𝐶 = 𝑥    )
22	21	in2	⊢ (    𝐴 ∈ 𝐵    ▶    ( 𝐶 = 𝐴 → [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 )    )
23		impbi	⊢ ( ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 → 𝐶 = 𝐴 ) → ( ( 𝐶 = 𝐴 → [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ) → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ 𝐶 = 𝐴 ) ) )
24	15 22 23	e11	⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ 𝐶 = 𝐴 )    )
25	24	in1	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 = 𝑥 ↔ 𝐶 = 𝐴 ) )