Colors of
variables: wff set class |
Syntax hints:
∧ wa 104 ↔ wb 105
∃wex 1492 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions:
df-bi 117 |
This theorem is referenced by: 19.29r
1621 19.42h
1687 19.42
1688 risset
2505 morex
2923 dfuni2
3813 eluni2
3815 unipr
3825 dfiun2g
3920 uniuni
4453 cnvco
4814 imadif
5298 funimaexglem
5301 pceu
12297 bdcuni
14667 bj-axun2
14706 |