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

Theorem rabbiia 3412
Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
Hypothesis
Ref Expression
rabbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rabbiia {𝑥𝐴𝜑} = {𝑥𝐴𝜓}

Proof of Theorem rabbiia
StepHypRef Expression
1 rabbiia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21pm5.32i 576 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rabbia2 3411 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  {crab 3408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-rab 3409
This theorem is referenced by:  rabbii  3414  fninfp  7121  fndifnfp  7123  nlimon  7788  dfom2  7805  rankval2  9755  ioopos  13342  prmreclem4  16792  acsfn1  17542  acsfn2  17544  logtayl  26018  ftalem3  26427  ppiub  26555  isuvtx  28346  vtxdginducedm1  28494  finsumvtxdg2size  28501  rgrusgrprc  28540  clwwlknclwwlkdif  28926  numclwwlkqhash  29322  ubthlem1  29815  xpinpreima  32490  xpinpreima2  32491  eulerpartgbij  32975  topdifinfeq  35824  rabimbieq  36714  rmydioph  41341  rmxdioph  41343  expdiophlem2  41349  expdioph  41350  alephiso3  41838  fsovrfovd  42288  k0004val0  42433  nzss  42604  hashnzfz  42607  fourierdlem90  44444  fourierdlem96  44450  fourierdlem97  44451  fourierdlem98  44452  fourierdlem99  44453  fourierdlem100  44454  fourierdlem109  44463  fourierdlem110  44464  fourierdlem112  44466  fourierdlem113  44467  sssmf  44986  dfodd6  45836  dfeven4  45837  dfeven2  45848  dfodd3  45849  dfeven3  45857  dfodd4  45858  dfodd5  45859
  Copyright terms: Public domain W3C validator