Theorem rabbiia 3420

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is referenced by:  rabbii  3421  fninfp  7172  fndifnfp  7174  nlimon  7843  dfom2  7860  rankval2  9786  ioopos  13446  prmreclem4  16974  acsfn1  17712  acsfn2  17714  logtayl  26825  ftalem3  27239  ppiub  27368  isuvtx  29745  vtxdginducedm1  29893  finsumvtxdg2size  29900  rgrusgrprc  29939  clwwlknclwwlkdif  30330  numclwwlkqhash  30726  ubthlem1  31222  psrbasfsupp  33901  xpinpreima  34296  xpinpreima2  34297  eulerpartgbij  34762  rankval2b  35492  dfscott2  35511  fineqvnttrclse  35537  topdifinfeq  38016  rabimbieq  38922  resuppsinopn  43144  rmydioph  43761  rmxdioph  43763  expdiophlem2  43769  expdioph  43770  alephiso3  44305  fsovrfovd  44755  k0004val0  44900  nzss  45047  hashnzfz  45050  fourierdlem90  46930  fourierdlem96  46936  fourierdlem97  46937  fourierdlem98  46938  fourierdlem99  46939  fourierdlem100  46940  fourierdlem109  46949  fourierdlem110  46950  fourierdlem112  46952  sssmf  47472  dfodd6  48422  dfeven4  48423  dfeven2  48434  dfodd3  48435  dfeven3  48443  dfodd4  48444  dfodd5  48445