Theorem rabbiia 3403

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  rabbii  3404  fninfp  7120  fndifnfp  7122  nlimon  7793  dfom2  7810  rankval2  9730  ioopos  13340  prmreclem4  16847  acsfn1  17584  acsfn2  17586  logtayl  26625  ftalem3  27041  ppiub  27171  isuvtx  29468  vtxdginducedm1  29617  finsumvtxdg2size  29624  rgrusgrprc  29663  clwwlknclwwlkdif  30054  numclwwlkqhash  30450  ubthlem1  30945  psrbasfsupp  33693  xpinpreima  34063  xpinpreima2  34064  eulerpartgbij  34529  rankval2b  35255  fineqvnttrclse  35280  topdifinfeq  37551  rabimbieq  38445  resuppsinopn  42614  rmydioph  43252  rmxdioph  43254  expdiophlem2  43260  expdioph  43261  alephiso3  43796  fsovrfovd  44246  k0004val0  44391  nzss  44554  hashnzfz  44557  fourierdlem90  46436  fourierdlem96  46442  fourierdlem97  46443  fourierdlem98  46444  fourierdlem99  46445  fourierdlem100  46446  fourierdlem109  46455  fourierdlem110  46456  fourierdlem112  46458  fourierdlem113  46459  sssmf  46978  dfodd6  47879  dfeven4  47880  dfeven2  47891  dfodd3  47892  dfeven3  47900  dfodd4  47901  dfodd5  47902