Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
vtocl3
Metamath Proof Explorer
Description: Implicit substitution of classes for setvar variables. (Contributed by NM , 3-Jun-1995) (Proof shortened by Andrew Salmon , 8-Jun-2011) Avoid
ax-10 and ax-11 . (Revised by GG , 20-Aug-2023) (Proof shortened by Wolf Lammen , 23-Aug-2023)
Ref
Expression
Hypotheses
vtocl3.1
⊢ A ∈ V
vtocl3.2
⊢ B ∈ V
vtocl3.3
⊢ C ∈ V
vtocl3.4
⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
vtocl3.5
⊢ φ
Assertion
vtocl3
⊢ ψ
Proof
Step
Hyp
Ref
Expression
1
vtocl3.1
⊢ A ∈ V
2
vtocl3.2
⊢ B ∈ V
3
vtocl3.3
⊢ C ∈ V
4
vtocl3.4
⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
5
vtocl3.5
⊢ φ
6
5
a1i
⊢ z = C → φ
7
4
3expa
⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
8
7
pm5.74da
⊢ x = A ∧ y = B → z = C → φ ↔ z = C → ψ
9
1 2 8 6
vtocl2
⊢ z = C → ψ
10
6 9
2thd
⊢ z = C → φ ↔ ψ
11
3 10 5
vtocl
⊢ ψ