Theorem rabbiia 3399

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396

This theorem is referenced by:  rabbii  3400  fninfp  7108  fndifnfp  7110  nlimon  7781  dfom2  7798  rankval2  9711  ioopos  13324  prmreclem4  16831  acsfn1  17567  acsfn2  17569  logtayl  26596  ftalem3  27012  ppiub  27142  isuvtx  29373  vtxdginducedm1  29522  finsumvtxdg2size  29529  rgrusgrprc  29568  clwwlknclwwlkdif  29959  numclwwlkqhash  30355  ubthlem1  30850  psrbasfsupp  33572  xpinpreima  33919  xpinpreima2  33920  eulerpartgbij  34385  rankval2b  35110  fineqvnttrclse  35144  topdifinfeq  37394  rabimbieq  38298  resuppsinopn  42466  rmydioph  43117  rmxdioph  43119  expdiophlem2  43125  expdioph  43126  alephiso3  43662  fsovrfovd  44112  k0004val0  44257  nzss  44420  hashnzfz  44423  fourierdlem90  46304  fourierdlem96  46310  fourierdlem97  46311  fourierdlem98  46312  fourierdlem99  46313  fourierdlem100  46314  fourierdlem109  46323  fourierdlem110  46324  fourierdlem112  46326  fourierdlem113  46327  sssmf  46846  dfodd6  47747  dfeven4  47748  dfeven2  47759  dfodd3  47760  dfeven3  47768  dfodd4  47769  dfodd5  47770