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 ( ( 𝑥𝑦𝑦𝑥𝑥 = 𝑦 ) ↔ ( ( 𝑥𝑦𝑦𝑥 ) ∨ 𝑥 = 𝑦 ) )
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 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 ( 𝐴𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥𝑦𝑦𝑥𝑥 = 𝑦 ) ↔ ( 𝑥𝐴𝐴𝑥𝑥 = 𝐴 ) ) )