This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Classes Class equality eqrdav
Description: Deduce equality of classes from an equivalence of membership that
depends on the membership variable. (Contributed by NM , 7-Nov-2008)
(Proof shortened by Wolf Lammen , 19-Nov-2019)
Ref
Expression
Hypotheses
eqrdav.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐶 )
eqrdav.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 )
eqrdav.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
Assertion
eqrdav ⊢ ( 𝜑 → 𝐴 = 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
eqrdav.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐶 )
2
eqrdav.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 )
3
eqrdav.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
4
1 2 3
bibiad ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
5
4
eqrdv ⊢ ( 𝜑 → 𝐴 = 𝐵 )