Theorem rabbiia 3447

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444

This theorem is referenced by:  rabbii  3449  fninfp  7208  fndifnfp  7210  nlimon  7888  dfom2  7905  rankval2  9887  ioopos  13484  prmreclem4  16966  acsfn1  17719  acsfn2  17721  logtayl  26720  ftalem3  27136  ppiub  27266  isuvtx  29430  vtxdginducedm1  29579  finsumvtxdg2size  29586  rgrusgrprc  29625  clwwlknclwwlkdif  30011  numclwwlkqhash  30407  ubthlem1  30902  xpinpreima  33852  xpinpreima2  33853  eulerpartgbij  34337  topdifinfeq  37316  rabimbieq  38207  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  alephiso3  43521  fsovrfovd  43971  k0004val0  44116  nzss  44286  hashnzfz  44289  fourierdlem90  46117  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem109  46136  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  sssmf  46659  dfodd6  47511  dfeven4  47512  dfeven2  47523  dfodd3  47524  dfeven3  47532  dfodd4  47533  dfodd5  47534