Metamath Proof Explorer


Theorem eqsbc3rVD

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

Ref Expression
Assertion eqsbc3rVD A B [˙A / x]˙ C = x C = A

Proof

Step Hyp Ref Expression
1 idn1 A B A B
2 eqsbc3 A B [˙A / x]˙ x = C A = C
3 1 2 e1a A B [˙A / x]˙ x = C A = C
4 eqcom C = x x = C
5 4 sbcbii [˙A / x]˙ C = x [˙A / x]˙ x = C
6 5 a1i A B [˙A / x]˙ C = x [˙A / x]˙ x = C
7 1 6 e1a A B [˙A / x]˙ C = x [˙A / x]˙ x = C
8 idn2 A B , [˙A / x]˙ C = x [˙A / x]˙ C = x
9 biimp [˙A / x]˙ C = x [˙A / x]˙ x = C [˙A / x]˙ C = x [˙A / x]˙ x = C
10 7 8 9 e12 A B , [˙A / x]˙ C = x [˙A / x]˙ x = C
11 biimp [˙A / x]˙ x = C A = C [˙A / x]˙ x = C A = C
12 3 10 11 e12 A B , [˙A / x]˙ C = x A = C
13 eqcom A = C C = A
14 12 13 e2bi A B , [˙A / x]˙ C = x C = A
15 14 in2 A B [˙A / x]˙ C = x C = A
16 idn2 A B , C = A C = A
17 16 13 e2bir A B , C = A A = C
18 biimpr [˙A / x]˙ x = C A = C A = C [˙A / x]˙ x = C
19 3 17 18 e12 A B , C = A [˙A / x]˙ x = C
20 biimpr [˙A / x]˙ C = x [˙A / x]˙ x = C [˙A / x]˙ x = C [˙A / x]˙ C = x
21 7 19 20 e12 A B , C = A [˙A / x]˙ C = x
22 21 in2 A B C = A [˙A / x]˙ C = x
23 impbi [˙A / x]˙ C = x C = A C = A [˙A / x]˙ C = x [˙A / x]˙ C = x C = A
24 15 22 23 e11 A B [˙A / x]˙ C = x C = A
25 24 in1 A B [˙A / x]˙ C = x C = A