Theorem rabbiia 3436

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-rab 3433

This theorem is referenced by:  rabbii  3438  fninfp  7171  fndifnfp  7173  nlimon  7839  dfom2  7856  rankval2  9812  ioopos  13400  prmreclem4  16851  acsfn1  17604  acsfn2  17606  logtayl  26167  ftalem3  26576  ppiub  26704  isuvtx  28649  vtxdginducedm1  28797  finsumvtxdg2size  28804  rgrusgrprc  28843  clwwlknclwwlkdif  29229  numclwwlkqhash  29625  ubthlem1  30118  xpinpreima  32881  xpinpreima2  32882  eulerpartgbij  33366  topdifinfeq  36226  rabimbieq  37114  rmydioph  41743  rmxdioph  41745  expdiophlem2  41751  expdioph  41752  alephiso3  42300  fsovrfovd  42750  k0004val0  42895  nzss  43066  hashnzfz  43069  fourierdlem90  44902  fourierdlem96  44908  fourierdlem97  44909  fourierdlem98  44910  fourierdlem99  44911  fourierdlem100  44912  fourierdlem109  44921  fourierdlem110  44922  fourierdlem112  44924  fourierdlem113  44925  sssmf  45444  dfodd6  46295  dfeven4  46296  dfeven2  46307  dfodd3  46308  dfeven3  46316  dfodd4  46317  dfodd5  46318