Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ↔ wb 176
∧ wa 358 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 177 df-an 360 |
This theorem is referenced by: 3simpa
952 reurex
2826 eqimss
3324 pssss
3365 eldifi
3389 inss1
3476 ssunsn2
3866 fnfun
5182 ffn
5224 f1f
5259 f1of1
5287 f1ofo
5294 nfvres
5353 ressnop0
5437 isof1o
5489 1stfo
5506 oprabid
5551 brtxp
5784 otelins2
5792 otelins3
5793 oqelins4
5795 weds
5939 ersym
5953 nchoicelem4
6293 nchoicelem8
6297 nchoicelem9
6298 nchoicelem19
6308 fnfreclem3
6320 |