Theorem rabbiia 3440

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437

This theorem is referenced by:  rabbii  3442  fninfp  7194  fndifnfp  7196  nlimon  7872  dfom2  7889  rankval2  9858  ioopos  13464  prmreclem4  16957  acsfn1  17704  acsfn2  17706  logtayl  26702  ftalem3  27118  ppiub  27248  isuvtx  29412  vtxdginducedm1  29561  finsumvtxdg2size  29568  rgrusgrprc  29607  clwwlknclwwlkdif  29998  numclwwlkqhash  30394  ubthlem1  30889  xpinpreima  33905  xpinpreima2  33906  eulerpartgbij  34374  topdifinfeq  37351  rabimbieq  38252  resuppsinopn  42393  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  alephiso3  43572  fsovrfovd  44022  k0004val0  44167  nzss  44336  hashnzfz  44339  fourierdlem90  46211  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem100  46221  fourierdlem109  46230  fourierdlem110  46231  fourierdlem112  46233  fourierdlem113  46234  sssmf  46753  dfodd6  47624  dfeven4  47625  dfeven2  47636  dfodd3  47637  dfeven3  47645  dfodd4  47646  dfodd5  47647