Metamath Proof Explorer


Theorem dfrdg3

Description: Generalization of dfrdg2 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg3 rec F I = f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y

Proof

Step Hyp Ref Expression
1 dfrdg2 I V rec F I = f | x On f Fn x y x f y = if y = I if Lim y f y F f y
2 iftrue I V if I V I = I
3 2 ifeq1d I V if y = if I V I if Lim y f y F f y = if y = I if Lim y f y F f y
4 3 eqeq2d I V f y = if y = if I V I if Lim y f y F f y f y = if y = I if Lim y f y F f y
5 4 ralbidv I V y x f y = if y = if I V I if Lim y f y F f y y x f y = if y = I if Lim y f y F f y
6 5 anbi2d I V f Fn x y x f y = if y = if I V I if Lim y f y F f y f Fn x y x f y = if y = I if Lim y f y F f y
7 6 rexbidv I V x On f Fn x y x f y = if y = if I V I if Lim y f y F f y x On f Fn x y x f y = if y = I if Lim y f y F f y
8 7 abbidv I V f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y = f | x On f Fn x y x f y = if y = I if Lim y f y F f y
9 8 unieqd I V f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y = f | x On f Fn x y x f y = if y = I if Lim y f y F f y
10 1 9 eqtr4d I V rec F I = f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y
11 0ex V
12 dfrdg2 V rec F = f | x On f Fn x y x f y = if y = if Lim y f y F f y
13 11 12 ax-mp rec F = f | x On f Fn x y x f y = if y = if Lim y f y F f y
14 rdgprc ¬ I V rec F I = rec F
15 iffalse ¬ I V if I V I =
16 15 ifeq1d ¬ I V if y = if I V I if Lim y f y F f y = if y = if Lim y f y F f y
17 16 eqeq2d ¬ I V f y = if y = if I V I if Lim y f y F f y f y = if y = if Lim y f y F f y
18 17 ralbidv ¬ I V y x f y = if y = if I V I if Lim y f y F f y y x f y = if y = if Lim y f y F f y
19 18 anbi2d ¬ I V f Fn x y x f y = if y = if I V I if Lim y f y F f y f Fn x y x f y = if y = if Lim y f y F f y
20 19 rexbidv ¬ I V x On f Fn x y x f y = if y = if I V I if Lim y f y F f y x On f Fn x y x f y = if y = if Lim y f y F f y
21 20 abbidv ¬ I V f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y = f | x On f Fn x y x f y = if y = if Lim y f y F f y
22 21 unieqd ¬ I V f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y = f | x On f Fn x y x f y = if y = if Lim y f y F f y
23 13 14 22 3eqtr4a ¬ I V rec F I = f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y
24 10 23 pm2.61i rec F I = f | x On f Fn x y x f y = if y = if I V I if Lim y f y F f y