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  6605  fndifnfp  6607  nlimon  7217  dfom2  7233  rankval2  8856  ioopos  12463  prmreclem4  15845  acsfn1  16543  acsfn2  16545  logtayl  24626  ftalem3  25021  ppiub  25149  isuvtx  26518  vtxdginducedm1  26670  finsumvtxdg2size  26677  rgrusgrprc  26716  clwwlknclwwlkdif  27121  clwwlknclwwlkdifsOLD  27123  numclwwlkqhash  27557  ubthlem1  28056  xpinpreima  30282  xpinpreima2  30283  eulerpartgbij  30764  topdifinfeq  33527  rabimbieq  34358  rmydioph  38101  rmxdioph  38103  expdiophlem2  38109  expdioph  38110  fsovrfovd  38823  k0004val0  38972  nzss  39036  hashnzfz  39039  fourierdlem90  40934  fourierdlem96  40940  fourierdlem97  40941  fourierdlem98  40942  fourierdlem99  40943  fourierdlem100  40944  fourierdlem109  40953  fourierdlem110  40954  fourierdlem112  40956  fourierdlem113  40957  sssmf  41471  dfodd6  42078  dfeven4  42079  dfeven2  42090  dfodd3  42091  dfeven3  42098  dfodd4  42099  dfodd5  42100
  Copyright terms: Public domain W3C validator