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 ) ) ) |
Ref | Expression | ||
---|---|---|---|
Assertion | sbcoreleleqVD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcor | |
|
2 | 1 | a1i | |
3 | df-3or | |
|
4 | 3 | bicomi | |
5 | 4 | sbcbii | |
6 | 5 | a1i | |
7 | sbcor | |
|
8 | 7 | a1i | |
9 | 8 | orbi1d | |
10 | 2 6 9 | 3bitr3d | |
11 | df-3or | |
|
12 | 10 11 | bitr4di | |
13 | 12 | dfvd1ir | |
14 | sbcel2gv | |
|
15 | 14 | dfvd1ir | |
16 | sbcel1v | |
|
17 | eqsbc2 | |
|
18 | 17 | dfvd1ir | |
19 | 3orbi123 | |
|
20 | 19 | 3impexpbicomi | |
21 | 15 16 18 20 | e101 | |
22 | biantr | |
|
23 | 13 21 22 | e11an | |
24 | 23 | in1 | |