# 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

### Proof

Step Hyp Ref Expression
1 sbcor
2 1 a1i
3 df-3or ${⊢}\left({x}\in {y}\vee {y}\in {x}\vee {x}={y}\right)↔\left(\left({x}\in {y}\vee {y}\in {x}\right)\vee {x}={y}\right)$
4 3 bicomi ${⊢}\left(\left({x}\in {y}\vee {y}\in {x}\right)\vee {x}={y}\right)↔\left({x}\in {y}\vee {y}\in {x}\vee {x}={y}\right)$
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 syl6bbr
13 12 dfvd1ir
14 sbcel2gv
15 14 dfvd1ir
16 sbcel1v
17 eqsbc3r
18 17 dfvd1ir
19 3orbi123
20 19 3impexpbicomi
21 15 16 18 20 e101
22 biantr
23 13 21 22 e11an
24 23 in1