Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∧ wa 396 ≠ wne 2940
∀wral 3061 ∅c0 4322 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-9 2116
ax-12 2171 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-ne 2941 df-ral 3062 df-dif 3951 df-nul 4323 |
This theorem is referenced by: raaanv
4521 raltpd
4785 iinrab
5072 iindif2
5080 iinin2
5081 reusv2lem5
5400 xpiindi
5835 dfpo2
6295 fint
6770 ixpiin
8920 neips
22624 txflf
23517 isclmp
24620 diaglbN
40012 dihglbcpreN
40257 2reuimp
45902 |