Metamath Proof Explorer
< Previous
Next >
Nearby theorems
Mirrors
>
Home
>
MPE Home
>
Th. List
> r19.27zv
Unicode version
Theorem
r19.27zv
3929
Description:
Restricted quantifier version of Theorem 19.27 of [
Margaris
] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.)
Assertion
Ref
Expression
r19.27zv
Distinct variable
groups:
,
,
Proof of Theorem
r19.27zv
Step
Hyp
Ref
Expression
1
r19.3rzv
3922
. . 3
2
1
anbi2d
703
. 2
3
r19.26
2984
. 2
4
2
,
3
syl6rbbr
264
1
Colors of variables:
wff
setvar
class
Syntax hints:
->
wi
4
<->
wb
184
/\
wa
369
=/=
wne
2652
A.
wral
2807
c0
3784
This theorem is referenced by:
raaanv
3938
txflf
20507
dfso3
29097
dibglbN
36893
This theorem was proved from axioms:
ax-mp
5
ax-1
6
ax-2
7
ax-3
8
ax-gen
1618
ax-4
1631
ax-5
1704
ax-6
1747
ax-7
1790
ax-10
1837
ax-11
1842
ax-12
1854
ax-13
1999
ax-ext
2435
This theorem depends on definitions:
df-bi
185
df-or
370
df-an
371
df-tru
1398
df-ex
1613
df-nf
1617
df-sb
1740
df-clab
2443
df-cleq
2449
df-clel
2452
df-nfc
2607
df-ne
2654
df-ral
2812
df-v
3111
df-dif
3478
df-nul
3785
Copyright terms:
Public domain
W3C validator