Metamath Proof Explorer

Theorem or2expropbilem2

Description: Lemma 2 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem2 
|- ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x ( <. A , B >. = <. a , b >. /\ ph )
2 nfv 
 |-  F/ y ( <. A , B >. = <. a , b >. /\ ph )
3 nfv 
 |-  F/ a <. A , B >. = <. x , y >.
4 nfcv 
 |-  F/_ a y
5 nfsbc1v 
 |-  F/ a [. x / a ]. ph
6 4 5 nfsbcw 
 |-  F/ a [. y / b ]. [. x / a ]. ph
7 3 6 nfan 
 |-  F/ a ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
8 nfv 
 |-  F/ b <. A , B >. = <. x , y >.
9 nfsbc1v 
 |-  F/ b [. y / b ]. [. x / a ]. ph
10 8 9 nfan 
 |-  F/ b ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
11 opeq12 
 |-  ( ( a = x /\ b = y ) -> <. a , b >. = <. x , y >. )
12 11 eqeq2d 
 |-  ( ( a = x /\ b = y ) -> ( <. A , B >. = <. a , b >. <-> <. A , B >. = <. x , y >. ) )
13 sbceq1a 
 |-  ( a = x -> ( ph <-> [. x / a ]. ph ) )
14 sbceq1a 
 |-  ( b = y -> ( [. x / a ]. ph <-> [. y / b ]. [. x / a ]. ph ) )
15 13 14 sylan9bb 
 |-  ( ( a = x /\ b = y ) -> ( ph <-> [. y / b ]. [. x / a ]. ph ) )
16 12 15 anbi12d 
 |-  ( ( a = x /\ b = y ) -> ( ( <. A , B >. = <. a , b >. /\ ph ) <-> ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
17 1 2 7 10 16 cbvex2v 
 |-  ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) )