Theorem 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	3	biimpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
5	4	impancom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) )
6	1 5	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
7	3	biimprd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) )
8	7	impancom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
9	2 8	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
10	6 9	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
11	10	eqrdv	⊢ ( 𝜑 → 𝐴 = 𝐵 )