Theorem rabbiia 3424

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-rab 3421

This theorem is referenced by:  rabbii  3426  fninfp  7171  fndifnfp  7173  nlimon  7851  dfom2  7868  rankval2  9837  ioopos  13446  prmreclem4  16944  acsfn1  17678  acsfn2  17680  logtayl  26626  ftalem3  27042  ppiub  27172  isuvtx  29379  vtxdginducedm1  29528  finsumvtxdg2size  29535  rgrusgrprc  29574  clwwlknclwwlkdif  29965  numclwwlkqhash  30361  ubthlem1  30856  xpinpreima  33942  xpinpreima2  33943  eulerpartgbij  34409  topdifinfeq  37373  rabimbieq  38274  resuppsinopn  42373  rmydioph  43005  rmxdioph  43007  expdiophlem2  43013  expdioph  43014  alephiso3  43550  fsovrfovd  44000  k0004val0  44145  nzss  44308  hashnzfz  44311  fourierdlem90  46192  fourierdlem96  46198  fourierdlem97  46199  fourierdlem98  46200  fourierdlem99  46201  fourierdlem100  46202  fourierdlem109  46211  fourierdlem110  46212  fourierdlem112  46214  fourierdlem113  46215  sssmf  46734  dfodd6  47618  dfeven4  47619  dfeven2  47630  dfodd3  47631  dfeven3  47639  dfodd4  47640  dfodd5  47641