Metamath Proof Explorer


Theorem tz6.26OLD

Description: Obsolete proof of tz6.26 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion tz6.26OLD R We A R Se A B A B y B Pred R B y =

Proof

Step Hyp Ref Expression
1 wereu2 R We A R Se A B A B ∃! y B x B ¬ x R y
2 reurex ∃! y B x B ¬ x R y y B x B ¬ x R y
3 1 2 syl R We A R Se A B A B y B x B ¬ x R y
4 rabeq0 x B | x R y = x B ¬ x R y
5 dfrab3 x B | x R y = B x | x R y
6 vex y V
7 6 dfpred2 Pred R B y = B x | x R y
8 5 7 eqtr4i x B | x R y = Pred R B y
9 8 eqeq1i x B | x R y = Pred R B y =
10 4 9 bitr3i x B ¬ x R y Pred R B y =
11 10 rexbii y B x B ¬ x R y y B Pred R B y =
12 3 11 sylib R We A R Se A B A B y B Pred R B y =