Theorem rabbiia 3403

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  rabbii  3404  fninfp  7120  fndifnfp  7122  nlimon  7793  dfom2  7810  rankval2  9732  ioopos  13342  prmreclem4  16849  acsfn1  17586  acsfn2  17588  logtayl  26627  ftalem3  27043  ppiub  27173  isuvtx  29470  vtxdginducedm1  29619  finsumvtxdg2size  29626  rgrusgrprc  29665  clwwlknclwwlkdif  30056  numclwwlkqhash  30452  ubthlem1  30947  psrbasfsupp  33695  xpinpreima  34065  xpinpreima2  34066  eulerpartgbij  34531  rankval2b  35257  fineqvnttrclse  35282  topdifinfeq  37557  rabimbieq  38452  resuppsinopn  42639  rmydioph  43277  rmxdioph  43279  expdiophlem2  43285  expdioph  43286  alephiso3  43821  fsovrfovd  44271  k0004val0  44416  nzss  44579  hashnzfz  44582  fourierdlem90  46461  fourierdlem96  46467  fourierdlem97  46468  fourierdlem98  46469  fourierdlem99  46470  fourierdlem100  46471  fourierdlem109  46480  fourierdlem110  46481  fourierdlem112  46483  fourierdlem113  46484  sssmf  47003  dfodd6  47904  dfeven4  47905  dfeven2  47916  dfodd3  47917  dfeven3  47925  dfodd4  47926  dfodd5  47927