Metamath Proof Explorer

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 
|- ( A e. B -> ( [. A / x ]. C = x <-> C = A ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A e. B ->. A e. B ).
2 eqsbc1 
 |-  ( A e. B -> ( [. A / x ]. x = C <-> A = C ) )
3 1 2 e1a 
 |-  (. A e. 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 e. B -> ( [. A / x ]. C = x <-> [. A / x ]. x = C ) )
7 1 6 e1a 
 |-  (. A e. B ->. ( [. A / x ]. C = x <-> [. A / x ]. x = C ) ).
8 idn2 
 |-  (. A e. 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 e. 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 e. B ,. [. A / x ]. C = x ->. A = C ).
13 eqcom 
 |-  ( A = C <-> C = A )
14 12 13 e2bi 
 |-  (. A e. B ,. [. A / x ]. C = x ->. C = A ).
15 14 in2 
 |-  (. A e. B ->. ( [. A / x ]. C = x -> C = A ) ).
16 idn2 
 |-  (. A e. B ,. C = A ->. C = A ).
17 16 13 e2bir 
 |-  (. A e. 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 e. 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 e. B ,. C = A ->. [. A / x ]. C = x ).
22 21 in2 
 |-  (. A e. 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 e. B ->. ( [. A / x ]. C = x <-> C = A ) ).
25 24 in1 
 |-  ( A e. B -> ( [. A / x ]. C = x <-> C = A ) )