Metamath Proof Explorer

Theorem sbcoreleleq

Description: Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcoreleleq 
|- ( A e. V -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )

Proof

Step Hyp Ref Expression
1 sbc3or 
 |-  ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) )
2 sbcel2gv 
 |-  ( A e. V -> ( [. A / y ]. x e. y <-> x e. A ) )
3 sbcel1v 
 |-  ( [. A / y ]. y e. x <-> A e. x )
4 3 a1i 
 |-  ( A e. V -> ( [. A / y ]. y e. x <-> A e. x ) )
5 eqsbc2 
 |-  ( A e. V -> ( [. A / y ]. x = y <-> x = A ) )
6 3orbi123 
 |-  ( ( ( [. A / y ]. x e. y <-> x e. A ) /\ ( [. A / y ]. y e. x <-> A e. x ) /\ ( [. A / y ]. x = y <-> x = A ) ) -> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )
7 6 3impexpbicomi 
 |-  ( ( [. A / y ]. x e. y <-> x e. A ) -> ( ( [. A / y ]. y e. x <-> A e. x ) -> ( ( [. A / y ]. x = y <-> x = A ) -> ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ) ) )
8 2 4 5 7 syl3c 
 |-  ( A e. V -> ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) )
9 1 8 bitr4id 
 |-  ( A e. V -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )