Theorem cleqrd 1100

Description: Deduce equality of sets from equivalence of membership.

Hypothesis

Ref	Expression
cleqrd.1	⊢ (φ → (x ∈ A ↔ x ∈ B))

Assertion

Ref	Expression
cleqrd	⊢ (φ → A = B)

Distinct variable group(s):   x,A   x,B   φ,x

Proof of Theorem cleqrd

Step	Hyp	Ref	Expression
1		cleqrd.1	. . 3 ⊢ (φ → (x ∈ A ↔ x ∈ B))
2	1	19.21aiv 943	. 2 ⊢ (φ → ∀x(x ∈ A ↔ x ∈ B))
3		dfcleq 1098	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4	2, 3	sylibr 175	1 ⊢ (φ → A = B)

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  uneq1 1605  ineq1 1638  unineq 1680  iunconst 2000  iindif2 2033  iununi 2037  iunpw 2040  onpwsuc 2315  ordsucun 2333  opthprc 2457  imadif 2714  tz6.12-1 2842  fconstfv 2903  erthi 3218  pw2en 3348  genpass 3906  1idpr 3927  ocin 5177  shscomt 5284  spansncol 5473

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-cleq 1097

metamath.org