MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabbiia Structured version   Visualization version   GIF version

Theorem rabbiia 3324
Description: Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rabbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rabbiia {𝑥𝐴𝜑} = {𝑥𝐴𝜓}

Proof of Theorem rabbiia
StepHypRef Expression
1 rabbiia.1 . . . 4 (𝑥𝐴 → (𝜑𝜓))
21pm5.32i 672 . . 3 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32abbii 2877 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3059 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
5 df-rab 3059 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
63, 4, 53eqtr4i 2792 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  {cab 2746  {crab 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-rab 3059
This theorem is referenced by:  rabbii  3325  elneldisjOLD  4108  elnelunOLD  4109  fninfp  6604  fndifnfp  6606  nlimon  7216  dfom2  7232  rankval2  8854  ioopos  12443  prmreclem4  15825  acsfn1  16523  acsfn2  16525  logtayl  24605  ftalem3  25000  ppiub  25128  isuvtx  26497  vtxdginducedm1  26649  finsumvtxdg2size  26656  rgrusgrprc  26695  clwwlknclwwlkdif  27100  clwwlknclwwlkdifsOLD  27102  numclwwlkqhash  27536  ubthlem1  28035  xpinpreima  30261  xpinpreima2  30262  eulerpartgbij  30743  topdifinfeq  33509  rabimbieq  34340  rmydioph  38083  rmxdioph  38085  expdiophlem2  38091  expdioph  38092  fsovrfovd  38805  k0004val0  38954  nzss  39018  hashnzfz  39021  fourierdlem90  40916  fourierdlem96  40922  fourierdlem97  40923  fourierdlem98  40924  fourierdlem99  40925  fourierdlem100  40926  fourierdlem109  40935  fourierdlem110  40936  fourierdlem112  40938  fourierdlem113  40939  sssmf  41453  dfodd6  42060  dfeven4  42061  dfeven2  42072  dfodd3  42073  dfeven3  42080  dfodd4  42081  dfodd5  42082
  Copyright terms: Public domain W3C validator