Description: Obsolete version of fvpr2 as of 26-Sep-2024. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fvpr2.1 | |- B e. _V |
|
| fvpr2.2 | |- D e. _V |
||
| Assertion | fvpr2OLD | |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvpr2.1 | |- B e. _V |
|
| 2 | fvpr2.2 | |- D e. _V |
|
| 3 | prcom | |- { <. A , C >. , <. B , D >. } = { <. B , D >. , <. A , C >. } |
|
| 4 | 3 | fveq1i | |- ( { <. A , C >. , <. B , D >. } ` B ) = ( { <. B , D >. , <. A , C >. } ` B ) |
| 5 | necom | |- ( A =/= B <-> B =/= A ) |
|
| 6 | 1 2 | fvpr1 | |- ( B =/= A -> ( { <. B , D >. , <. A , C >. } ` B ) = D ) |
| 7 | 5 6 | sylbi | |- ( A =/= B -> ( { <. B , D >. , <. A , C >. } ` B ) = D ) |
| 8 | 4 7 | syl5eq | |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) |