Theorem rabbiia 3422

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {crab 3418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rab 3419

This theorem is used by:  rabbii  3423  fninfp  7178  fndifnfp  7180  nlimon  7853  dfom2  7870  rankval2  9797  ioopos  13471  prmreclem4  17005  acsfn1  17743  acsfn2  17745  logtayl  26880  ftalem3  27294  ppiub  27423  isuvtx  29807  vtxdginducedm1  29955  finsumvtxdg2size  29962  rgrusgrprc  30001  clwwlknclwwlkdif  30401  numclwwlkqhash  30801  ubthlem1  31297  psrbasfsupp  33969  xpinpreima  34364  xpinpreima2  34365  eulerpartgbij  34831  rankval2b  35554  dfscott2  35573  fineqvnttrclse  35598  topdifinfeq  38057  rabimbieq  38964  resuppsinopn  43201  rmydioph  43818  rmxdioph  43820  expdiophlem2  43826  expdioph  43827  alephiso3  44362  fsovrfovd  44812  k0004val0  44957  nzss  45104  hashnzfz  45107  fourierdlem90  46987  fourierdlem96  46993  fourierdlem97  46994  fourierdlem98  46995  fourierdlem99  46996  fourierdlem100  46997  fourierdlem109  47006  fourierdlem110  47007  fourierdlem112  47009  sssmf  47529  dfodd6  48479  dfeven4  48480  dfeven2  48491  dfodd3  48492  dfeven3  48500  dfodd4  48501  dfodd5  48502