Theorem eqrdv 2168

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
eqrdv	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	alrimiv 1867	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2164	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 133	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqrdav  2169  csbcomg  3072  csbabg  3110  uneq1  3274  ineq1  3321  difin2  3389  difsn  3715  intmin4  3857  iunconstm  3879  iinconstm  3880  dfiun2g  3903  iindif2m  3938  iinin2m  3939  iunxsng  3946  iunxsngf  3948  iunpw  4463  opthprc  4660  inimasn  5026  dmsnopg  5080  dfco2a  5109  iotaeq  5166  fun11iun  5461  ssimaex  5555  unpreima  5618  respreima  5621  fconstfvm  5711  reldm  6162  rntpos  6233  frecsuclem  6382  iserd  6535  erth  6553  ecidg  6573  mapdm0  6637  map0e  6660  ixpiinm  6698  fifo  6953  ordiso2  7008  ctssdccl  7084  ctssdc  7086  genpassl  7473  genpassu  7474  1idprl  7539  1idpru  7540  sup3exmid  8860  eqreznegel  9560  iccid  9869  fzsplit2  9993  fzsn  10009  fzpr  10020  uzsplit  10035  fzoval  10091  frec2uzrand  10348  infssuzex  11891  mhmpropd  12676  discld  12889  restsn  12933  restdis  12937  cndis  12994  cnpdis  12995  tx1cn  13022  tx2cn  13023  blpnf  13153  blininf  13177  blres  13187  xmetec  13190  metrest  13259  xmetxpbl  13261  cnbl0  13287  reopnap  13291  bl2ioo  13295  cncfmet  13332  limcdifap  13384