Colors of
variables: wff set class |
Syntax hints: ⊤wtru 1354 Ⅎwnf 1460
Ⅎwnfc 2306
∀wral 2455 |
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-7 1448
ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-nf 1461 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 |
This theorem is referenced by: nfra2xy
2519 rspc2
2853 sbcralt
3040 sbcralg
3042 raaanlem
3529 nfint
3855 nfiinxy
3914 nfpo
4302 nfso
4303 nfse
4342 nffrfor
4349 nfwe
4356 ralxpf
4774 funimaexglem
5300 fun11iun
5483 dff13f
5771 nfiso
5807 mpoeq123
5934 nfofr
6089 fmpox
6201 nfrecs
6308 xpf1o
6844 ac6sfi
6898 ismkvnex
7153 lble
8904 fzrevral
10105 nfsum1
11364 nfsum
11365 fsum2dlemstep
11442 fisumcom2
11446 nfcprod1
11562 nfcprod
11563 bezoutlemmain
11999 cnmpt21
13794 setindis
14722 bdsetindis
14724 strcollnfALT
14741 isomninnlem
14781 iswomninnlem
14800 ismkvnnlem
14803 |