Step |
Hyp |
Ref |
Expression |
1 |
|
ssopab2b |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) ) |
2 |
|
ssopab2b |
|- ( { <. x , y >. | ps } C_ { <. x , y >. | ph } <-> A. x A. y ( ps -> ph ) ) |
3 |
1 2
|
anbi12i |
|- ( ( { <. x , y >. | ph } C_ { <. x , y >. | ps } /\ { <. x , y >. | ps } C_ { <. x , y >. | ph } ) <-> ( A. x A. y ( ph -> ps ) /\ A. x A. y ( ps -> ph ) ) ) |
4 |
|
eqss |
|- ( { <. x , y >. | ph } = { <. x , y >. | ps } <-> ( { <. x , y >. | ph } C_ { <. x , y >. | ps } /\ { <. x , y >. | ps } C_ { <. x , y >. | ph } ) ) |
5 |
|
2albiim |
|- ( A. x A. y ( ph <-> ps ) <-> ( A. x A. y ( ph -> ps ) /\ A. x A. y ( ps -> ph ) ) ) |
6 |
3 4 5
|
3bitr4i |
|- ( { <. x , y >. | ph } = { <. x , y >. | ps } <-> A. x A. y ( ph <-> ps ) ) |