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
⊢ Ⅎ 𝑥 𝜓
vtoclf.2
⊢ 𝐴 ∈ V
vtoclf.3
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
vtoclf.4
⊢ 𝜑
Assertion
vtoclfOLD
⊢ 𝜓
Proof
Step
Hyp
Ref
Expression
1
vtoclf.1
⊢ Ⅎ 𝑥 𝜓
2
vtoclf.2
⊢ 𝐴 ∈ V
3
vtoclf.3
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4
vtoclf.4
⊢ 𝜑
5
2
isseti
⊢ ∃ 𝑥 𝑥 = 𝐴
6
3
biimpd
⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
7
5 6
eximii
⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
8
1 7
19.36i
⊢ ( ∀ 𝑥 𝜑 → 𝜓 )
9
8 4
mpg
⊢ 𝜓