Description: Ordered pair member of the partial isomorphism H for atom argument not under W . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihelval2.l | |
|
dihelval2.a | |
||
dihelval2.h | |
||
dihelval2.p | |
||
dihelval2.t | |
||
dihelval2.e | |
||
dihelval2.i | |
||
dihelval2.g | |
||
dihelval2.f | |
||
dihelval2.s | |
||
Assertion | dihopelvalcqat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihelval2.l | |
|
2 | dihelval2.a | |
|
3 | dihelval2.h | |
|
4 | dihelval2.p | |
|
5 | dihelval2.t | |
|
6 | dihelval2.e | |
|
7 | dihelval2.i | |
|
8 | dihelval2.g | |
|
9 | dihelval2.f | |
|
10 | dihelval2.s | |
|
11 | eqid | |
|
12 | 1 2 3 11 7 | dihvalcqat | |
13 | 12 | eleq2d | |
14 | 1 2 3 4 5 6 11 8 9 10 | dicopelval2 | |
15 | 13 14 | bitrd | |