Step |
Hyp |
Ref |
Expression |
1 |
|
prprspr2 |
|- ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 } |
2 |
1
|
rabeq2i |
|- ( p e. ( PrPairs ` V ) <-> ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) ) |
3 |
2
|
a1i |
|- ( V e. W -> ( p e. ( PrPairs ` V ) <-> ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) ) ) |
4 |
3
|
anbi1d |
|- ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) /\ ph ) ) ) |
5 |
|
anass |
|- ( ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) /\ ph ) <-> ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) |
6 |
4 5
|
bitrdi |
|- ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) ) |
7 |
6
|
eubidv |
|- ( V e. W -> ( E! p ( p e. ( PrPairs ` V ) /\ ph ) <-> E! p ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) ) |
8 |
|
df-reu |
|- ( E! p e. ( PrPairs ` V ) ph <-> E! p ( p e. ( PrPairs ` V ) /\ ph ) ) |
9 |
|
df-reu |
|- ( E! p e. ( Pairs ` V ) ( ( # ` p ) = 2 /\ ph ) <-> E! p ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) |
10 |
7 8 9
|
3bitr4g |
|- ( V e. W -> ( E! p e. ( PrPairs ` V ) ph <-> E! p e. ( Pairs ` V ) ( ( # ` p ) = 2 /\ ph ) ) ) |