This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elequ12

Description: An identity law for the non-logical predicate, which combines elequ1 and elequ2 . The analogous theorems for class terms are eleq1 , eleq2 , and eleq12 respectively. (Contributed by BJ, 29-Sep-2019)

		Ref	Expression
	Assertion	elequ12	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑡 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡 ) )

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
2		elequ2	⊢ ( 𝑧 = 𝑡 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡 ) )
3	1 2	sylan9bb	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑡 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡 ) )