Theorem rabbiia 3406

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3403

This theorem is referenced by:  rabbii  3408  fninfp  7130  fndifnfp  7132  nlimon  7807  dfom2  7824  rankval2  9747  ioopos  13361  prmreclem4  16866  acsfn1  17602  acsfn2  17604  logtayl  26602  ftalem3  27018  ppiub  27148  isuvtx  29375  vtxdginducedm1  29524  finsumvtxdg2size  29531  rgrusgrprc  29570  clwwlknclwwlkdif  29958  numclwwlkqhash  30354  ubthlem1  30849  xpinpreima  33889  xpinpreima2  33890  eulerpartgbij  34356  topdifinfeq  37331  rabimbieq  38233  resuppsinopn  42344  rmydioph  42996  rmxdioph  42998  expdiophlem2  43004  expdioph  43005  alephiso3  43541  fsovrfovd  43991  k0004val0  44136  nzss  44299  hashnzfz  44302  fourierdlem90  46187  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem100  46197  fourierdlem109  46206  fourierdlem110  46207  fourierdlem112  46209  fourierdlem113  46210  sssmf  46729  dfodd6  47631  dfeven4  47632  dfeven2  47643  dfodd3  47644  dfeven3  47652  dfodd4  47653  dfodd5  47654