Colors of
variables: wff set class |
Syntax hints: wtru 1354
wnf 1460
wnfc 2306
wrex 2456 |
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-rex 2461 |
This theorem is referenced by: r19.12
2583 sbcrext
3040 nfuni
3815 nfiunxy
3912 rexxpf
4774 abrexex2g
6120 abrexex2
6124 nfrecs
6307 fimaxre2
11234 nfsum
11364 nfcprod1
11561 nfcprod
11562 bezoutlemmain
11998 ctiunctlemfo
12439 bj-findis
14701 strcollnfALT
14708 |