Theorem rabbiia 3398

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3395

This theorem is referenced by:  rabbii  3400  fninfp  7110  fndifnfp  7112  nlimon  7784  dfom2  7801  rankval2  9714  ioopos  13327  prmreclem4  16831  acsfn1  17567  acsfn2  17569  logtayl  26567  ftalem3  26983  ppiub  27113  isuvtx  29340  vtxdginducedm1  29489  finsumvtxdg2size  29496  rgrusgrprc  29535  clwwlknclwwlkdif  29923  numclwwlkqhash  30319  ubthlem1  30814  psrbasfsupp  33545  xpinpreima  33879  xpinpreima2  33880  eulerpartgbij  34346  fineqvnttrclse  35083  topdifinfeq  37334  rabimbieq  38236  resuppsinopn  42346  rmydioph  42997  rmxdioph  42999  expdiophlem2  43005  expdioph  43006  alephiso3  43542  fsovrfovd  43992  k0004val0  44137  nzss  44300  hashnzfz  44303  fourierdlem90  46187  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem100  46197  fourierdlem109  46206  fourierdlem110  46207  fourierdlem112  46209  fourierdlem113  46210  sssmf  46729  dfodd6  47631  dfeven4  47632  dfeven2  47643  dfodd3  47644  dfeven3  47652  dfodd4  47653  dfodd5  47654