Theorem rabbiia 3419

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561   ∈ wcel 2143  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-rab 3416

This theorem is referenced by:  rabbii  3420  fninfp  7159  fndifnfp  7161  nlimon  7832  dfom2  7849  rankval2  9777  ioopos  13429  prmreclem4  16956  acsfn1  17694  acsfn2  17696  logtayl  26726  ftalem3  27140  ppiub  27269  isuvtx  29597  vtxdginducedm1  29745  finsumvtxdg2size  29752  rgrusgrprc  29791  clwwlknclwwlkdif  30182  numclwwlkqhash  30578  ubthlem1  31074  psrbasfsupp  33809  xpinpreima  34204  xpinpreima2  34205  eulerpartgbij  34670  rankval2b  35396  fineqvnttrclse  35421  topdifinfeq  37845  rabimbieq  38753  resuppsinopn  42973  rmydioph  43592  rmxdioph  43594  expdiophlem2  43600  expdioph  43601  alephiso3  44136  fsovrfovd  44586  k0004val0  44731  nzss  44894  hashnzfz  44897  fourierdlem90  46771  fourierdlem96  46777  fourierdlem97  46778  fourierdlem98  46779  fourierdlem99  46780  fourierdlem100  46781  fourierdlem109  46790  fourierdlem110  46791  fourierdlem112  46793  sssmf  47313  dfodd6  48260  dfeven4  48261  dfeven2  48272  dfodd3  48273  dfeven3  48281  dfodd4  48282  dfodd5  48283