Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
∀wral 3061 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions:
df-bi 206 df-ex 1783 df-ral 3062 |
This theorem is referenced by: rspec2
3261 vtoclri
3544 wfis
6310 wfis2f
6313 wfis2
6315 isarep2
6593 mpoexw
8012 ecopover
8763 frins
9693 alephsuc2
10021 indstr
12846 reltxrnmnf
13267 ackbijnn
15718 mrelatglb0
18455 0frgp
19566 iccpnfcnv
24323 prter2
37389 natlocalincr
45201 natglobalincr
45202 |