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  6566  1idpru  6567  eqreznegel  8325  iccid  8564  fzsplit2  8684  fzsn  8699  fzpr  8709  uzsplit  8724  fzoval  8775  frec2uzrand  8872
 Copyright terms: Public domain W3C validator