This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem raleqbidvvOLD

Description: Obsolete version of raleqbidvv as of 9-Mar-2025. (Contributed by BJ, 22-Sep-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses raleqbidvv.1 
|- ( ph -> A = B )
raleqbidvv.2 
|- ( ph -> ( ps <-> ch ) )
Assertion raleqbidvvOLD 
|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Proof

Step Hyp Ref Expression
1 raleqbidvv.1 
 |-  ( ph -> A = B )
2 raleqbidvv.2 
 |-  ( ph -> ( ps <-> ch ) )
3 2 alrimiv 
 |-  ( ph -> A. x ( ps <-> ch ) )
4 dfcleq 
 |-  ( A = B <-> A. x ( x e. A <-> x e. B ) )
5 1 4 sylib 
 |-  ( ph -> A. x ( x e. A <-> x e. B ) )
6 19.26 
 |-  ( A. x ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) <-> ( A. x ( ps <-> ch ) /\ A. x ( x e. A <-> x e. B ) ) )
7 3 5 6 sylanbrc 
 |-  ( ph -> A. x ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) )
8 imbi12 
 |-  ( ( x e. A <-> x e. B ) -> ( ( ps <-> ch ) -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) ) )
9 8 impcom 
 |-  ( ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )
10 7 9 sylg 
 |-  ( ph -> A. x ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )
11 albi 
 |-  ( A. x ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
12 10 11 syl 
 |-  ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
13 df-ral 
 |-  ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
14 df-ral 
 |-  ( A. x e. B ch <-> A. x ( x e. B -> ch ) )
15 12 13 14 3bitr4g 
 |-  ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )