r19.2z - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem r19.2z 2337

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1026). The restricted version is valid only when the domain of quantification is not empty.

**Assertion**
Ref	Expression
r19.2z	$/\$

Distinct variable group:

**Proof of Theorem r19.2z**
Step	Hyp	Ref	Expression
1		df-ral 1641	. . . 4
2		exintr 1113	. . . 4 $/\$
3	1, 2	sylbi 199	. . 3 $/\$
4		ne0 2278	. . 3
5		df-rex 1642	. . 3 $/\$
6	3, 4, 5	3imtr4g 551	. 2
7	6	impcom 351	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wal 951

wcel 955

wex 977

wne 1577

wral 1637

wrex 1638

c0 2270

This theorem is referenced by: intssuni 2545 alephval2 4874 cfeq0 4886 cfsuc 4887 isgrp2i 8011 fgsb 10444 fgsb2 10449

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-v 1803 df-dif 2039 df-nul 2271