Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∀wal 1351
Ⅎwnf 1460 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-5 1447 ax-gen 1449 ax-4 1510 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 |
This theorem is referenced by: axc4i
1542 19.32r
1680 cbv3
1742 sbbid
1846 sbalyz
1999 dvelimdf
2016 dvelimor
2018 nf5d
2025 abbid
2294 nfcd
2314 nfabdw
2338 ralrimi
2548 r19.32r
2623 ceqsalg
2765 ceqsex
2775 vtocldf
2788 elrab3t
2892 morex
2921 sbciedf
2998 csbiebt
3096 csbiedf
3097 ssrd
3160 rgenm
3525 invdisj
3997 ssopab2b
4276 eusv2nf
4456 sniota
5207 imadif
5296 funimaexglem
5299 eusvobj1
5861 ssoprab2b
5931 ovmpodxf
5999 |