Theorem wl-dfcleq.basic

Description: This is a copy of dfcleq in main. It is not sufficient to avoid reproving ax-8 as shown in in-ax8 . (Contributed by NM, 15-Sep-1993) (Revised by BJ, 24-Jun-2019)

	Ref	Expression
Assertion	wl-dfcleq.basic	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		axextb	⊢ ( 𝑦 = 𝑧 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧 ) )
2		axextb	⊢ ( 𝑡 = 𝑡 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡 ) )
3	1 2	wl-df.cleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )