Theorem rabbiia 3401

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 3400	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-rab 3398

This theorem is referenced by:  rabbii  3402  fninfp  7118  fndifnfp  7120  nlimon  7791  dfom2  7808  rankval2  9728  ioopos  13338  prmreclem4  16845  acsfn1  17582  acsfn2  17584  logtayl  26623  ftalem3  27039  ppiub  27169  isuvtx  29417  vtxdginducedm1  29566  finsumvtxdg2size  29573  rgrusgrprc  29612  clwwlknclwwlkdif  30003  numclwwlkqhash  30399  ubthlem1  30894  psrbasfsupp  33642  xpinpreima  34012  xpinpreima2  34013  eulerpartgbij  34478  rankval2b  35204  fineqvnttrclse  35229  topdifinfeq  37494  rabimbieq  38388  resuppsinopn  42560  rmydioph  43198  rmxdioph  43200  expdiophlem2  43206  expdioph  43207  alephiso3  43742  fsovrfovd  44192  k0004val0  44337  nzss  44500  hashnzfz  44503  fourierdlem90  46382  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem100  46392  fourierdlem109  46401  fourierdlem110  46402  fourierdlem112  46404  fourierdlem113  46405  sssmf  46924  dfodd6  47825  dfeven4  47826  dfeven2  47837  dfodd3  47838  dfeven3  47846  dfodd4  47847  dfodd5  47848