rexnal - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem rexnal 1646

Description: Relationship between restricted universal and existential quantifiers.

**Assertion**
Ref	Expression
rexnal

**Proof of Theorem rexnal**
Step	Hyp	Ref	Expression
1		exanali 1039	. 2 $/\$
2		df-rex 1642	. 2 $/\$
3		df-ral 1641	. . 3
4	3	negbii 187	. 2
5	1, 2, 4	3bitr4 183	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 146 $/\$ wa 223

wal 951

wcel 955

wex 977

wral 1637

wrex 1638

This theorem is referenced by: dfral2 1647 rexanali 1676 uni0b 2513 iundif2 2600 elpwunsn 2902 ixp0 4345 isfinite2 4523 unbndrank 4655 ac6n 4729 kmlem3 4739 kmlem7 4743 kmlem8 4744 kmlem13 4749 alephval2 4874 cfeq0 4886 arch 6018 xrsupsslem 6023 xrinfmsslem 6024 supxrbnd 6038 supxrbnd1 6042 supxrbnd2 6043 climunii 7035 climubi 7089 infxpidmlem8 7502 fctop 7592 cctop 7594 bcthlem33 7965 nmounbi 8371 hlimunii 9029 nmcopexlem1 9866 nmcfnexlem1 9895 iintlem1 10476

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 960 ax-4 970 ax-5o 972

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 978 df-ral 1641 df-rex 1642