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  28652  vtxdginducedm1  28800  finsumvtxdg2size  28807  rgrusgrprc  28846  clwwlknclwwlkdif  29232  numclwwlkqhash  29628  ubthlem1  30123  xpinpreima  32886  xpinpreima2  32887  eulerpartgbij  33371  topdifinfeq  36231  rabimbieq  37119  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  alephiso3  42310  fsovrfovd  42760  k0004val0  42905  nzss  43076  hashnzfz  43079  fourierdlem90  44912  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem100  44922  fourierdlem109  44931  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  sssmf  45454  dfodd6  46305  dfeven4  46306  dfeven2  46317  dfodd3  46318  dfeven3  46326  dfodd4  46327  dfodd5  46328