Theorem eqrdv 2229

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1395   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqrdav  2230  eqabdv  2360  csbcomg  3150  csbabg  3189  uneq1  3354  ineq1  3401  difin2  3469  difsn  3810  intmin4  3956  iunconstm  3978  iinconstm  3979  dfiun2g  4002  iindif2m  4038  iinin2m  4039  iunxsng  4046  iunxsngf  4048  iunpw  4577  opthprc  4777  inimasn  5154  dmsnopg  5208  dfco2a  5237  iotaeq  5295  fun11iun  5604  ssimaex  5707  unpreima  5772  respreima  5775  fconstfvm  5872  reldm  6349  rntpos  6423  frecsuclem  6572  iserd  6728  erth  6748  ecidg  6768  mapdm0  6832  map0e  6855  ixpiinm  6893  pw2f1odclem  7020  fifo  7179  ordiso2  7234  ctssdccl  7310  ctssdc  7312  finacn  7419  pw1if  7443  exmidapne  7479  acnccim  7491  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  sup3exmid  9137  eqreznegel  9848  iccid  10160  fzsplit2  10285  fzsn  10301  fzpr  10312  uzsplit  10327  fzoval  10383  infssuzex  10493  frec2uzrand  10667  bitsmod  12518  bitscmp  12520  divsfval  13412  mhmpropd  13550  eqgid  13814  ghmmhmb  13842  ghmpropd  13871  ablnsg  13922  opprsubgg  14099  opprunitd  14126  unitpropdg  14164  opprsubrngg  14227  subsubrng2  14231  subrngpropd  14232  subsubrg2  14262  subrgpropd  14269  rhmpropd  14270  lssats2  14430  lsspropdg  14447  discld  14862  restsn  14906  restdis  14910  cndis  14967  cnpdis  14968  tx1cn  14995  tx2cn  14996  blpnf  15126  blininf  15150  blres  15160  xmetec  15163  metrest  15232  xmetxpbl  15234  cnbl0  15260  reopnap  15272  bl2ioo  15276  cncfmet  15318  limcdifap  15388  gausslemma2dlem1a  15789  ushgredgedg  16079  ushgredgedgloop  16081  clwwlknun  16294