Metamath Proof Explorer


Theorem sbcoreleleqVD

Description: Virtual deduction proof of sbcoreleleq . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1:: |- (. A e. B ->. A e. B ).
2:1,?: e1a |- (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
3:1,?: e1a |- (. A e. B ->. ( [. A / y ]. y e. x <-> A e. x ) ).
4:1,?: e1a |- (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
5:2,3,4,?: e111 |- (. A e. B ->. ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
6:1,?: e1a |- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
7:5,6: e11 |- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ).
qed:7: |- ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcoreleleqVD AB[˙A/y]˙xyyxx=yxAAxx=A

Proof

Step Hyp Ref Expression
1 sbcor [˙A/y]˙xyyxx=y[˙A/y]˙xyyx[˙A/y]˙x=y
2 1 a1i AB[˙A/y]˙xyyxx=y[˙A/y]˙xyyx[˙A/y]˙x=y
3 df-3or xyyxx=yxyyxx=y
4 3 bicomi xyyxx=yxyyxx=y
5 4 sbcbii [˙A/y]˙xyyxx=y[˙A/y]˙xyyxx=y
6 5 a1i AB[˙A/y]˙xyyxx=y[˙A/y]˙xyyxx=y
7 sbcor [˙A/y]˙xyyx[˙A/y]˙xy[˙A/y]˙yx
8 7 a1i AB[˙A/y]˙xyyx[˙A/y]˙xy[˙A/y]˙yx
9 8 orbi1d AB[˙A/y]˙xyyx[˙A/y]˙x=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
10 2 6 9 3bitr3d AB[˙A/y]˙xyyxx=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
11 df-3or [˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
12 10 11 bitr4di AB[˙A/y]˙xyyxx=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
13 12 dfvd1ir AB[˙A/y]˙xyyxx=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
14 sbcel2gv AB[˙A/y]˙xyxA
15 14 dfvd1ir AB[˙A/y]˙xyxA
16 sbcel1v [˙A/y]˙yxAx
17 eqsbc2 AB[˙A/y]˙x=yx=A
18 17 dfvd1ir AB[˙A/y]˙x=yx=A
19 3orbi123 [˙A/y]˙xyxA[˙A/y]˙yxAx[˙A/y]˙x=yx=A[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=yxAAxx=A
20 19 3impexpbicomi [˙A/y]˙xyxA[˙A/y]˙yxAx[˙A/y]˙x=yx=AxAAxx=A[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
21 15 16 18 20 e101 ABxAAxx=A[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y
22 biantr [˙A/y]˙xyyxx=y[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=yxAAxx=A[˙A/y]˙xy[˙A/y]˙yx[˙A/y]˙x=y[˙A/y]˙xyyxx=yxAAxx=A
23 13 21 22 e11an AB[˙A/y]˙xyyxx=yxAAxx=A
24 23 in1 AB[˙A/y]˙xyyxx=yxAAxx=A