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∈B→[˙A/x]˙C=x↔C=A

Proof

Step Hyp Ref Expression
1 idn1 ⊢A∈B→A∈B
2 eqsbc1 ⊢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