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 V [˙A / y]˙ x y y x x = y x A A x x = A

Proof

Step Hyp Ref Expression
1 sbcel2gv A V [˙A / y]˙ x y x A
2 sbcel1v [˙A / y]˙ y x A x
3 2 a1i A V [˙A / y]˙ y x A x
4 eqsbc3r A V [˙A / y]˙ x = y x = A
5 3orbi123 [˙A / y]˙ x y x A [˙A / y]˙ y x A x [˙A / y]˙ x = y x = A [˙A / y]˙ x y [˙A / y]˙ y x [˙A / y]˙ x = y x A A x x = A
6 5 3impexpbicomi [˙A / y]˙ x y x A [˙A / y]˙ y x A x [˙A / y]˙ x = y x = A x A A x x = A [˙A / y]˙ x y [˙A / y]˙ y x [˙A / y]˙ x = y
7 1 3 4 6 syl3c A V x A A x x = A [˙A / y]˙ x y [˙A / y]˙ y x [˙A / y]˙ x = y
8 sbc3or [˙A / y]˙ x y y x x = y [˙A / y]˙ x y [˙A / y]˙ y x [˙A / y]˙ x = y
9 7 8 syl6rbbr A V [˙A / y]˙ x y y x x = y x A A x x = A