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

Theorem eqrdv 2021
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 1737 . 2 (φx(x Ax B))
3 dfcleq 2017 . 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 1375
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 1401  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-cleq 2016
This theorem is referenced by:  eqrdav  2022  csbcomg  2849  csbabg  2883  uneq1  3066  ineq1  3107  difin2  3175  difsn  3474  intmin4  3616  iunconstm  3638  iinconstm  3639  dfiun2g  3662  iindif2m  3697  iinin2m  3698  iunxsng  3705  iunpw  4159  opthprc  4316  inimasn  4666  dmsnopg  4717  dfco2a  4746  iotaeq  4800  fun11iun  5070  ssimaex  5157  unpreima  5215  respreima  5218  fconstfvm  5302  reldm  5732  rntpos  5791  frecsuclem3  5901  iserd  6038  erth  6055
  Copyright terms: Public domain W3C validator