Theorem moi

Description: Equality implied by "at most one". (Contributed by NM, 18-Feb-2006)

	Ref	Expression
Hypotheses	moi.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	moi.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion	moi	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		moi.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		moi.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
3	1 2	mob	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝐴 = 𝐵 ↔ 𝜒 ) )
4	3	biimprd	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝐴 = 𝐵 ) )
5	4	3expia	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ) → ( 𝜓 → ( 𝜒 → 𝐴 = 𝐵 ) ) )
6	5	impd	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜒 ) → 𝐴 = 𝐵 ) )
7	6	3impia	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∃* 𝑥 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝐴 = 𝐵 )