Theorem eqrdv 2175

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351   = 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-5 1447  ax-gen 1449  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqrdav  2176  csbcomg  3081  csbabg  3119  uneq1  3283  ineq1  3330  difin2  3398  difsn  3730  intmin4  3873  iunconstm  3895  iinconstm  3896  dfiun2g  3919  iindif2m  3955  iinin2m  3956  iunxsng  3963  iunxsngf  3965  iunpw  4481  opthprc  4678  inimasn  5047  dmsnopg  5101  dfco2a  5130  iotaeq  5187  fun11iun  5483  ssimaex  5578  unpreima  5642  respreima  5645  fconstfvm  5735  reldm  6187  rntpos  6258  frecsuclem  6407  iserd  6561  erth  6579  ecidg  6599  mapdm0  6663  map0e  6686  ixpiinm  6724  fifo  6979  ordiso2  7034  ctssdccl  7110  ctssdc  7112  exmidapne  7259  genpassl  7523  genpassu  7524  1idprl  7589  1idpru  7590  sup3exmid  8914  eqreznegel  9614  iccid  9925  fzsplit2  10050  fzsn  10066  fzpr  10077  uzsplit  10092  fzoval  10148  frec2uzrand  10405  infssuzex  11950  mhmpropd  12857  eqgid  13085  opprunitd  13279  unitpropdg  13317  subsubrg2  13367  subrgpropd  13369  discld  13639  restsn  13683  restdis  13687  cndis  13744  cnpdis  13745  tx1cn  13772  tx2cn  13773  blpnf  13903  blininf  13927  blres  13937  xmetec  13940  metrest  14009  xmetxpbl  14011  cnbl0  14037  reopnap  14041  bl2ioo  14045  cncfmet  14082  limcdifap  14134