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

Theorem eqrdv 2020
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 1736 . 2 (φx(x Ax B))
3 dfcleq 2016 . 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 1226   = wceq 1228   wcel 1374
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 1316  ax-gen 1318  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqrdav  2021  csbcomg  2848  csbabg  2882  uneq1  3065  ineq1  3106  difin2  3174  difsn  3473  intmin4  3615  iunconstm  3637  iinconstm  3638  dfiun2g  3661  iindif2m  3696  iinin2m  3697  iunxsng  3704  iunpw  4159  opthprc  4316  inimasn  4666  dmsnopg  4717  dfco2a  4746  iotaeq  4800  fun11iun  5070  ssimaex  5157  unpreima  5215  respreima  5218  fconstfvm  5302  reldm  5733  rntpos  5792  frecsuclem3  5904  iserd  6041  erth  6059  ecidg  6079  genpassl  6377  genpassu  6378  1idprl  6427  1idpru  6428
  Copyright terms: Public domain W3C validator