Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
spcimgft
Next ⟩
spcimgfi1
Metamath Proof Explorer
Ascii
Unicode
Theorem
spcimgft
Description:
Closed theorem form of
spcimgf
.
(Contributed by
Wolf Lammen
, 28-Jul-2025)
Ref
Expression
Assertion
spcimgft
⊢
Ⅎ
_
x
A
∧
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
→
ψ
→
A
∈
V
→
∀
x
φ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
elissetv
⊢
A
∈
V
→
∃
y
y
=
A
2
cbvexeqsetf
⊢
Ⅎ
_
x
A
→
∃
x
x
=
A
↔
∃
y
y
=
A
3
1
2
imbitrrid
⊢
Ⅎ
_
x
A
→
A
∈
V
→
∃
x
x
=
A
4
pm2.04
⊢
x
=
A
→
φ
→
ψ
→
φ
→
x
=
A
→
ψ
5
4
al2imi
⊢
∀
x
x
=
A
→
φ
→
ψ
→
∀
x
φ
→
∀
x
x
=
A
→
ψ
6
19.23t
⊢
Ⅎ
x
ψ
→
∀
x
x
=
A
→
ψ
↔
∃
x
x
=
A
→
ψ
7
6
biimpd
⊢
Ⅎ
x
ψ
→
∀
x
x
=
A
→
ψ
→
∃
x
x
=
A
→
ψ
8
5
7
sylan9r
⊢
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
→
ψ
→
∀
x
φ
→
∃
x
x
=
A
→
ψ
9
8
com23
⊢
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
→
ψ
→
∃
x
x
=
A
→
∀
x
φ
→
ψ
10
3
9
sylan9
⊢
Ⅎ
_
x
A
∧
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
→
ψ
→
A
∈
V
→
∀
x
φ
→
ψ
11
10
anassrs
⊢
Ⅎ
_
x
A
∧
Ⅎ
x
ψ
∧
∀
x
x
=
A
→
φ
→
ψ
→
A
∈
V
→
∀
x
φ
→
ψ