Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
∀wral 3062 |
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 3063 |
This theorem is referenced by: rspec2
3277 vtoclri
3577 wfis
6357 wfis2f
6360 wfis2
6362 isarep2
6640 mpoexw
8065 ecopover
8815 frins
9747 alephsuc2
10075 indstr
12900 reltxrnmnf
13321 ackbijnn
15774 mrelatglb0
18514 0frgp
19647 iccpnfcnv
24460 prter2
37751 natlocalincr
45590 natglobalincr
45591 |