Metamath Proof Explorer


Theorem fnwe2val

Description: Lemma for fnwe2 . Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su z = F x S = U
fnwe2.t T = x y | F x R F y F x = F y x U y
Assertion fnwe2val a T b F a R F b F a = F b a F a / z S b

Proof

Step Hyp Ref Expression
1 fnwe2.su z = F x S = U
2 fnwe2.t T = x y | F x R F y F x = F y x U y
3 vex a V
4 vex b V
5 fveq2 x = a F x = F a
6 fveq2 y = b F y = F b
7 5 6 breqan12d x = a y = b F x R F y F a R F b
8 5 6 eqeqan12d x = a y = b F x = F y F a = F b
9 simpl x = a y = b x = a
10 fvex F x V
11 10 1 csbie F x / z S = U
12 5 csbeq1d x = a F x / z S = F a / z S
13 11 12 eqtr3id x = a U = F a / z S
14 13 adantr x = a y = b U = F a / z S
15 simpr x = a y = b y = b
16 9 14 15 breq123d x = a y = b x U y a F a / z S b
17 8 16 anbi12d x = a y = b F x = F y x U y F a = F b a F a / z S b
18 7 17 orbi12d x = a y = b F x R F y F x = F y x U y F a R F b F a = F b a F a / z S b
19 3 4 18 2 braba a T b F a R F b F a = F b a F a / z S b