Theorem rabbiia 3394

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3391

This theorem is referenced by:  rabbii  3395  fninfp  7124  fndifnfp  7126  nlimon  7797  dfom2  7814  rankval2  9737  ioopos  13372  prmreclem4  16885  acsfn1  17622  acsfn2  17624  logtayl  26641  ftalem3  27056  ppiub  27185  isuvtx  29482  vtxdginducedm1  29631  finsumvtxdg2size  29638  rgrusgrprc  29677  clwwlknclwwlkdif  30068  numclwwlkqhash  30464  ubthlem1  30960  psrbasfsupp  33691  xpinpreima  34070  xpinpreima2  34071  eulerpartgbij  34536  rankval2b  35262  fineqvnttrclse  35288  topdifinfeq  37684  rabimbieq  38592  resuppsinopn  42813  rmydioph  43464  rmxdioph  43466  expdiophlem2  43472  expdioph  43473  alephiso3  44008  fsovrfovd  44458  k0004val0  44603  nzss  44766  hashnzfz  44769  fourierdlem90  46646  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem100  46656  fourierdlem109  46665  fourierdlem110  46666  fourierdlem112  46668  fourierdlem113  46669  sssmf  47188  dfodd6  48129  dfeven4  48130  dfeven2  48141  dfodd3  48142  dfeven3  48150  dfodd4  48151  dfodd5  48152