Metamath Proof Explorer

Theorem freq1

Description: Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997)

Ref Expression
Assertion freq1 
|- ( R = S -> ( R Fr A <-> S Fr A ) )

Proof

Step Hyp Ref Expression
1 breq 
 |-  ( R = S -> ( z R y <-> z S y ) )
2 1 notbid 
 |-  ( R = S -> ( -. z R y <-> -. z S y ) )
3 2 rexralbidv 
 |-  ( R = S -> ( E. y e. x A. z e. x -. z R y <-> E. y e. x A. z e. x -. z S y ) )
4 3 imbi2d 
 |-  ( R = S -> ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) ) )
5 4 albidv 
 |-  ( R = S -> ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) ) )
6 df-fr 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
7 df-fr 
 |-  ( S Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) )
8 5 6 7 3bitr4g 
 |-  ( R = S -> ( R Fr A <-> S Fr A ) )