Theorem eqriv 1477

Description: Infer equality of classes from equivalence of membership.

Hypothesis

Ref	Expression
eqri.1	|- (x e. A <-> x e. B)

Assertion

Ref	Expression
eqriv	|- A = B

Distinct variable groups:   x,A   x,B

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 1473	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
2		eqri.1	. 2 |- (x e. A <-> x e. B)
3	1, 2	mpgbir 990	1 |- A = B

Syntax hints:   <-> wb 146   = wceq 958   e. wcel 960

This theorem is referenced by:  eqid 1478  uneqri 2177  uncom 2179  incom 2211  ineqri 2212  dfss4 2245  dfun2 2246  dfin2 2247  difin 2248  indi 2254  undi 2255  unab 2270  inab 2271  pwv 2506  uniun 2523  intun 2566  intpr 2567  iunid 2607  iun0 2608  0iun 2609  iunin2 2613  iinun2 2614  iundif2 2615  iunxsn 2617  iunxun 2619  iinuni 2620  iinpw 2622  pwundif 2834  unon 3094  xp0r 3245  cnvuni 3307  dmun 3323  dmuni 3325  rnuni 3465  imaco 3507  rnco 3508  imaiun 3870  erdmrn 4282  mapval2 4341  mapixp 4368  jech9.3 4676  dfn2 6114  dfuz 6204  om2uzran 6301  qnnen 7504  pilem1 8666  circgrp 8735  choc0 9285  chocnul 9287  spanunsn 9497  lncnbd 9962  adjbd1o 10013  rnbra 10035  pjima 10099  ntunte 10434  dtopcl 10586

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-cleq 1472

Copyright terms: Public domain