Theorem rabbiia 3412

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rab 3409

This theorem is referenced by:  rabbii  3414  fninfp  7151  fndifnfp  7153  nlimon  7830  dfom2  7847  rankval2  9778  ioopos  13392  prmreclem4  16897  acsfn1  17629  acsfn2  17631  logtayl  26576  ftalem3  26992  ppiub  27122  isuvtx  29329  vtxdginducedm1  29478  finsumvtxdg2size  29485  rgrusgrprc  29524  clwwlknclwwlkdif  29915  numclwwlkqhash  30311  ubthlem1  30806  xpinpreima  33903  xpinpreima2  33904  eulerpartgbij  34370  topdifinfeq  37345  rabimbieq  38247  resuppsinopn  42358  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  alephiso3  43555  fsovrfovd  44005  k0004val0  44150  nzss  44313  hashnzfz  44316  fourierdlem90  46201  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem100  46211  fourierdlem109  46220  fourierdlem110  46221  fourierdlem112  46223  fourierdlem113  46224  sssmf  46743  dfodd6  47642  dfeven4  47643  dfeven2  47654  dfodd3  47655  dfeven3  47663  dfodd4  47664  dfodd5  47665