Metamath Proof Explorer
Table of Contents - 2.4.1. Introduce the Axiom of Union
- ax-un
- zfun
- axun2
- uniex2
- vuniex
- uniexg
- uniex
- uniexd
- unex
- tpex
- unexb
- unexg
- xpexg
- xpexd
- 3xpexg
- xpex
- unexd
- sqxpexg
- abnexg
- abnex
- snnex
- pwnex
- difex2
- difsnexi
- uniuni
- uniexr
- uniexb
- pwexr
- pwexb
- elpwpwel
- eldifpw
- elpwun
- pwuncl
- iunpw
- fr3nr
- epne3
- dfwe2