Theorem eqrdv 2202

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 1896	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2198	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1370   = wceq 1372   ∈ wcel 2175

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-5 1469  ax-gen 1471  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqrdav  2203  eqabdv  2333  csbcomg  3115  csbabg  3154  uneq1  3319  ineq1  3366  difin2  3434  difsn  3769  intmin4  3912  iunconstm  3934  iinconstm  3935  dfiun2g  3958  iindif2m  3994  iinin2m  3995  iunxsng  4002  iunxsngf  4004  iunpw  4526  opthprc  4725  inimasn  5099  dmsnopg  5153  dfco2a  5182  iotaeq  5239  fun11iun  5542  ssimaex  5639  unpreima  5704  respreima  5707  fconstfvm  5801  reldm  6271  rntpos  6342  frecsuclem  6491  iserd  6645  erth  6665  ecidg  6685  mapdm0  6749  map0e  6772  ixpiinm  6810  pw2f1odclem  6930  fifo  7081  ordiso2  7136  ctssdccl  7212  ctssdc  7214  finacn  7315  exmidapne  7371  acnccim  7383  genpassl  7636  genpassu  7637  1idprl  7702  1idpru  7703  sup3exmid  9029  eqreznegel  9734  iccid  10046  fzsplit2  10171  fzsn  10187  fzpr  10198  uzsplit  10213  fzoval  10269  infssuzex  10374  frec2uzrand  10548  bitsmod  12209  bitscmp  12211  divsfval  13102  mhmpropd  13240  eqgid  13504  ghmmhmb  13532  ghmpropd  13561  ablnsg  13612  opprsubgg  13788  opprunitd  13814  unitpropdg  13852  opprsubrngg  13915  subsubrng2  13919  subrngpropd  13920  subsubrg2  13950  subrgpropd  13957  rhmpropd  13958  lssats2  14118  lsspropdg  14135  discld  14550  restsn  14594  restdis  14598  cndis  14655  cnpdis  14656  tx1cn  14683  tx2cn  14684  blpnf  14814  blininf  14838  blres  14848  xmetec  14851  metrest  14920  xmetxpbl  14922  cnbl0  14948  reopnap  14960  bl2ioo  14964  cncfmet  15006  limcdifap  15076  gausslemma2dlem1a  15477