Description: Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elpreqpr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpri | |
|
2 | elex | |
|
3 | elpreqprlem | |
|
4 | eleq1 | |
|
5 | preq1 | |
|
6 | 5 | eqeq2d | |
7 | 6 | exbidv | |
8 | 4 7 | imbi12d | |
9 | 3 8 | mpbiri | |
10 | 9 | imp | |
11 | elpreqprlem | |
|
12 | prcom | |
|
13 | 12 | eqeq1i | |
14 | 13 | exbii | |
15 | 11 14 | sylib | |
16 | eleq1 | |
|
17 | preq1 | |
|
18 | 17 | eqeq2d | |
19 | 18 | exbidv | |
20 | 16 19 | imbi12d | |
21 | 15 20 | mpbiri | |
22 | 21 | imp | |
23 | 10 22 | jaoian | |
24 | 1 2 23 | syl2anc | |