Theorem rabbiia 3427

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 584	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rabbia2 3426	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424

This theorem is referenced by:  rabbii  3428  fninfp  7173  fndifnfp  7175  nlimon  7847  dfom2  7864  rankval2  9790  ioopos  13451  prmreclem4  16979  acsfn1  17717  acsfn2  17719  logtayl  26791  ftalem3  27205  ppiub  27334  isuvtx  29686  vtxdginducedm1  29834  finsumvtxdg2size  29841  rgrusgrprc  29880  clwwlknclwwlkdif  30271  numclwwlkqhash  30667  ubthlem1  31163  psrbasfsupp  33846  xpinpreima  34241  xpinpreima2  34242  eulerpartgbij  34707  rankval2b  35435  fineqvnttrclse  35470  topdifinfeq  37918  rabimbieq  38826  resuppsinopn  43048  rmydioph  43667  rmxdioph  43669  expdiophlem2  43675  expdioph  43676  alephiso3  44211  fsovrfovd  44661  k0004val0  44806  nzss  44953  hashnzfz  44956  fourierdlem90  46836  fourierdlem96  46842  fourierdlem97  46843  fourierdlem98  46844  fourierdlem99  46845  fourierdlem100  46846  fourierdlem109  46855  fourierdlem110  46856  fourierdlem112  46858  sssmf  47378  dfodd6  48325  dfeven4  48326  dfeven2  48337  dfodd3  48338  dfeven3  48346  dfodd4  48347  dfodd5  48348