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 574	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rabbia2 3436	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-rab 3434

This theorem is referenced by:  rabbii  3439  fninfp  7194  fndifnfp  7196  nlimon  7872  dfom2  7889  rankval2  9856  ioopos  13461  prmreclem4  16953  acsfn1  17706  acsfn2  17708  logtayl  26717  ftalem3  27133  ppiub  27263  isuvtx  29427  vtxdginducedm1  29576  finsumvtxdg2size  29583  rgrusgrprc  29622  clwwlknclwwlkdif  30008  numclwwlkqhash  30404  ubthlem1  30899  xpinpreima  33867  xpinpreima2  33868  eulerpartgbij  34354  topdifinfeq  37333  rabimbieq  38233  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  alephiso3  43549  fsovrfovd  43999  k0004val0  44144  nzss  44313  hashnzfz  44316  fourierdlem90  46152  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem100  46162  fourierdlem109  46171  fourierdlem110  46172  fourierdlem112  46174  fourierdlem113  46175  sssmf  46694  dfodd6  47562  dfeven4  47563  dfeven2  47574  dfodd3  47575  dfeven3  47583  dfodd4  47584  dfodd5  47585