ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqrdv GIF version

Theorem eqrdv 2138
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
StepHypRef Expression
1 eqrdv.1 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
21alrimiv 1847 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2134 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 133 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1330   = wceq 1332  wcel 1481
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 1424  ax-gen 1426  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  eqrdav  2139  csbcomg  3029  csbabg  3065  uneq1  3227  ineq1  3274  difin2  3342  difsn  3664  intmin4  3806  iunconstm  3828  iinconstm  3829  dfiun2g  3852  iindif2m  3887  iinin2m  3888  iunxsng  3895  iunxsngf  3897  iunpw  4408  opthprc  4597  inimasn  4963  dmsnopg  5017  dfco2a  5046  iotaeq  5103  fun11iun  5395  ssimaex  5489  unpreima  5552  respreima  5555  fconstfvm  5645  reldm  6091  rntpos  6161  frecsuclem  6310  iserd  6462  erth  6480  ecidg  6500  mapdm0  6564  map0e  6587  ixpiinm  6625  fifo  6875  ordiso2  6927  ctssdccl  7003  ctssdc  7005  genpassl  7355  genpassu  7356  1idprl  7421  1idpru  7422  sup3exmid  8738  eqreznegel  9432  iccid  9737  fzsplit2  9860  fzsn  9876  fzpr  9887  uzsplit  9902  fzoval  9955  frec2uzrand  10208  infssuzex  11676  discld  12342  restsn  12386  restdis  12390  cndis  12447  cnpdis  12448  tx1cn  12475  tx2cn  12476  blpnf  12606  blininf  12630  blres  12640  xmetec  12643  metrest  12712  xmetxpbl  12714  cnbl0  12740  reopnap  12744  bl2ioo  12748  cncfmet  12785  limcdifap  12837
  Copyright terms: Public domain W3C validator