Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ∧
wa 358 ∈ wcel 1710 ∃wrex 2616 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-11 1746 |
This theorem depends on definitions:
df-bi 177 df-an 360
df-ex 1542 df-nf 1545 df-ral 2620 df-rex 2621 |
This theorem is referenced by: rexlimdvaa
2740 rexlimivv
2744 rexlimdvv
2745 pw1disj
4168 leltfintr
4459 ncfinlower
4484 tfin11
4494 tfinpw1
4495 nnpweq
4524 sfin112
4530 sfindbl
4531 vfinspss
4552 vfinspeqtncv
4554 phi11lem1
4596 foco2
5427 f1elima
5475 ectocld
5992 ncssfin
6152 nntccl
6171 dflec2
6211 leaddc1
6215 leconnnc
6219 tlecg
6231 letc
6232 ce2le
6234 ce0lenc1
6240 nclenn
6250 lemuc1
6254 lecadd2
6267 ncslesuc
6268 nnc3n3p1
6279 nchoicelem17
6306 nchoicelem19
6308 nchoice
6309 dmfrec
6317 fnfreclem3
6320 |