Theorem eqriv 2174

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 2171	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1453	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1449  ax-ext 2159

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

This theorem is referenced by:  eqid  2177  sb8ab  2299  cbvabw  2300  cbvab  2301  vjust  2739  nfccdeq  2961  csbcow  3069  difeqri  3256  uneqri  3278  incom  3328  ineqri  3329  difin  3373  invdif  3378  indif  3379  difundi  3388  indifdir  3392  pwv  3809  uniun  3829  intun  3876  intpr  3877  iuncom  3893  iuncom4  3894  iun0  3944  0iun  3945  iunin2  3951  iunun  3966  iunxun  3967  iunxiun  3969  iinpw  3978  inuni  4156  unidif0  4168  unipw  4218  snnex  4449  unon  4511  xpiundi  4685  xpiundir  4686  0xp  4707  iunxpf  4776  cnvuni  4814  dmiun  4837  dmuni  4838  epini  5000  rniun  5040  cnvresima  5119  imaco  5135  rnco  5136  dfmpt3  5339  imaiun  5761  opabex3d  6122  opabex3  6123  ecid  6598  qsid  6600  mapval2  6678  ixpin  6723  dfz2  9325  dfrp2  10264  infssuzex  11950  1nprm  12114  infpn2  12457