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