Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | cnviin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |
|
2 | relcnv | |
|
3 | df-rel | |
|
4 | 2 3 | mpbi | |
5 | 4 | rgenw | |
6 | r19.2z | |
|
7 | 5 6 | mpan2 | |
8 | iinss | |
|
9 | 7 8 | syl | |
10 | df-rel | |
|
11 | 9 10 | sylibr | |
12 | opex | |
|
13 | eliin | |
|
14 | 12 13 | ax-mp | |
15 | vex | |
|
16 | vex | |
|
17 | 15 16 | opelcnv | |
18 | opex | |
|
19 | eliin | |
|
20 | 18 19 | ax-mp | |
21 | 15 16 | opelcnv | |
22 | 21 | ralbii | |
23 | 20 22 | bitri | |
24 | 14 17 23 | 3bitr4i | |
25 | 24 | eqrelriv | |
26 | 1 11 25 | sylancr | |