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

Theorem eqrdv 2035
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1 (φ → (x Ax B))
Assertion
Ref Expression
eqrdv (φA = B)
Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3 (φ → (x Ax B))
21alrimiv 1751 . 2 (φx(x Ax B))
3 dfcleq 2031 . 2 (A = Bx(x Ax B))
42, 3sylibr 137 1 (φA = B)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1240   = wceq 1242   wcel 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqrdav  2036  csbcomg  2867  csbabg  2901  uneq1  3084  ineq1  3125  difin2  3193  difsn  3492  intmin4  3634  iunconstm  3656  iinconstm  3657  dfiun2g  3680  iindif2m  3715  iinin2m  3716  iunxsng  3723  iunpw  4177  opthprc  4334  inimasn  4684  dmsnopg  4735  dfco2a  4764  iotaeq  4818  fun11iun  5090  ssimaex  5177  unpreima  5235  respreima  5238  fconstfvm  5322  reldm  5754  rntpos  5813  frecsuclem3  5929  iserd  6068  erth  6086  ecidg  6106  genpassl  6507  genpassu  6508  1idprl  6564  1idpru  6565  eqreznegel  8285  iccid  8524  fzsplit2  8644  fzsn  8659  fzpr  8669  uzsplit  8684  fzoval  8735  frec2uzrand  8832
  Copyright terms: Public domain W3C validator