Theorem rabbiia 3437

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

Step	Hyp	Ref	Expression
1		rabbiia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 576	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rabbia2 3436	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {crab 3433

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434

This theorem is referenced by:  rabbii  3439  fninfp  7172  fndifnfp  7174  nlimon  7840  dfom2  7857  rankval2  9813  ioopos  13401  prmreclem4  16852  acsfn1  17605  acsfn2  17607  logtayl  26168  ftalem3  26579  ppiub  26707  isuvtx  28683  vtxdginducedm1  28831  finsumvtxdg2size  28838  rgrusgrprc  28877  clwwlknclwwlkdif  29263  numclwwlkqhash  29659  ubthlem1  30154  xpinpreima  32917  xpinpreima2  32918  eulerpartgbij  33402  topdifinfeq  36279  rabimbieq  37167  rmydioph  41801  rmxdioph  41803  expdiophlem2  41809  expdioph  41810  alephiso3  42358  fsovrfovd  42808  k0004val0  42953  nzss  43124  hashnzfz  43127  fourierdlem90  44960  fourierdlem96  44966  fourierdlem97  44967  fourierdlem98  44968  fourierdlem99  44969  fourierdlem100  44970  fourierdlem109  44979  fourierdlem110  44980  fourierdlem112  44982  fourierdlem113  44983  sssmf  45502  dfodd6  46353  dfeven4  46354  dfeven2  46365  dfodd3  46366  dfeven3  46374  dfodd4  46375  dfodd5  46376