Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
vtoclfOLD
Metamath Proof Explorer
Description: Obsolete version of vtoclf as of 26-Jan-2025. (Contributed by NM , 30-Aug-1993) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
vtoclf.1
⊢ Ⅎ x ψ
vtoclf.2
⊢ A ∈ V
vtoclf.3
⊢ x = A → φ ↔ ψ
vtoclf.4
⊢ φ
Assertion
vtoclfOLD
⊢ ψ
Proof
Step
Hyp
Ref
Expression
1
vtoclf.1
⊢ Ⅎ x ψ
2
vtoclf.2
⊢ A ∈ V
3
vtoclf.3
⊢ x = A → φ ↔ ψ
4
vtoclf.4
⊢ φ
5
2
isseti
⊢ ∃ x x = A
6
3
biimpd
⊢ x = A → φ → ψ
7
5 6
eximii
⊢ ∃ x φ → ψ
8
1 7
19.36i
⊢ ∀ x φ → ψ
9
8 4
mpg
⊢ ψ