Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
elabg
Metamath Proof Explorer
Description: Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of Quine p. 44. (Contributed by NM , 14-Apr-1995)
Remove dependency on ax-13 . (Revised by Steven Nguyen , 23-Nov-2022)
Ref
Expression
Hypothesis
elabg.1
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion
elabg
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
elabg.1
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2
nfab1
⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
3
2
nfel2
⊢ Ⅎ 𝑥 𝐴 ∈ { 𝑥 ∣ 𝜑 }
4
nfv
⊢ Ⅎ 𝑥 𝜓
5
3 4
nfbi
⊢ Ⅎ 𝑥 ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
6
eleq1
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
7
6 1
bibi12d
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) ↔ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
8
abid
⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9
5 7 8
vtoclg1f
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )