Theorem eqriv 2186

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqriv.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
eqriv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2183	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1464	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  eqid  2189  sb8ab  2311  cbvabw  2312  cbvab  2313  vjust  2753  nfccdeq  2975  csbcow  3083  difeqri  3270  uneqri  3292  incom  3342  ineqri  3343  difin  3387  invdif  3392  indif  3393  difundi  3402  indifdir  3406  pwv  3823  uniun  3843  intun  3890  intpr  3891  iuncom  3907  iuncom4  3908  iun0  3958  0iun  3959  iunin2  3965  iunun  3980  iunxun  3981  iunxiun  3983  iinpw  3992  inuni  4173  unidif0  4185  unipw  4235  snnex  4466  unon  4528  xpiundi  4702  xpiundir  4703  0xp  4724  iunxpf  4793  cnvuni  4831  dmiun  4854  dmuni  4855  epini  5017  rniun  5057  cnvresima  5136  imaco  5152  rnco  5153  dfmpt3  5357  imaiun  5782  opabex3d  6146  opabex3  6147  ecid  6624  qsid  6626  mapval2  6704  ixpin  6749  dfz2  9355  dfrp2  10294  infssuzex  11982  1nprm  12146  infpn2  12507