Theorem rabbiia 3395

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-rab 3392

This theorem is referenced by:  rabbii  3396  fninfp  7119  fndifnfp  7121  nlimon  7792  dfom2  7809  rankval2  9734  ioopos  13369  prmreclem4  16882  acsfn1  17619  acsfn2  17621  logtayl  26643  ftalem3  27057  ppiub  27186  isuvtx  29483  vtxdginducedm1  29631  finsumvtxdg2size  29638  rgrusgrprc  29677  clwwlknclwwlkdif  30068  numclwwlkqhash  30464  ubthlem1  30960  psrbasfsupp  33704  xpinpreima  34099  xpinpreima2  34100  eulerpartgbij  34565  rankval2b  35289  fineqvnttrclse  35314  topdifinfeq  37721  rabimbieq  38629  resuppsinopn  42849  rmydioph  43468  rmxdioph  43470  expdiophlem2  43476  expdioph  43477  alephiso3  44012  fsovrfovd  44462  k0004val0  44607  nzss  44770  hashnzfz  44773  fourierdlem90  46647  fourierdlem96  46653  fourierdlem97  46654  fourierdlem98  46655  fourierdlem99  46656  fourierdlem100  46657  fourierdlem109  46666  fourierdlem110  46667  fourierdlem112  46669  fourierdlem113  46670  sssmf  47189  dfodd6  48136  dfeven4  48137  dfeven2  48148  dfodd3  48149  dfeven3  48157  dfodd4  48158  dfodd5  48159