Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2099
∀wral 3056 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-12 2164 |
This theorem depends on definitions:
df-bi 206 df-ex 1775 df-ral 3057 |
This theorem is referenced by: rspec2
3271 vtoclri
3571 wfis
6355 wfis2f
6358 wfis2
6360 isarep2
6638 mpoexw
8077 ecopover
8831 frins
9767 alephsuc2
10095 indstr
12922 reltxrnmnf
13345 ackbijnn
15798 mrelatglb0
18544 0frgp
19725 iccpnfcnv
24856 prter2
38290 natlocalincr
46185 natglobalincr
46186 |