Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
ceqsralv
Next ⟩
gencl
Metamath Proof Explorer
Ascii
Unicode
Theorem
ceqsralv
Description:
Restricted quantifier version of
ceqsalv
.
(Contributed by
NM
, 21-Jun-2013)
Ref
Expression
Hypothesis
ceqsralv.2
⊢
x
=
A
→
φ
↔
ψ
Assertion
ceqsralv
⊢
A
∈
B
→
∀
x
∈
B
x
=
A
→
φ
↔
ψ
Proof
Step
Hyp
Ref
Expression
1
ceqsralv.2
⊢
x
=
A
→
φ
↔
ψ
2
nfv
⊢
Ⅎ
x
ψ
3
1
ax-gen
⊢
∀
x
x
=
A
→
φ
↔
ψ
4
ceqsralt
⊢
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
↔
ψ
∧
A
∈
B
→
∀
x
∈
B
x
=
A
→
φ
↔
ψ
5
2
3
4
mp3an12
⊢
A
∈
B
→
∀
x
∈
B
x
=
A
→
φ
↔
ψ