Theorem rabbiia 3393

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390

This theorem is referenced by:  rabbii  3394  fninfp  7129  fndifnfp  7131  nlimon  7802  dfom2  7819  rankval2  9742  ioopos  13377  prmreclem4  16890  acsfn1  17627  acsfn2  17629  logtayl  26624  ftalem3  27038  ppiub  27167  isuvtx  29464  vtxdginducedm1  29612  finsumvtxdg2size  29619  rgrusgrprc  29658  clwwlknclwwlkdif  30049  numclwwlkqhash  30445  ubthlem1  30941  psrbasfsupp  33672  xpinpreima  34050  xpinpreima2  34051  eulerpartgbij  34516  rankval2b  35242  fineqvnttrclse  35268  topdifinfeq  37666  rabimbieq  38574  resuppsinopn  42795  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  alephiso3  43986  fsovrfovd  44436  k0004val0  44581  nzss  44744  hashnzfz  44747  fourierdlem90  46624  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem100  46634  fourierdlem109  46643  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  sssmf  47166  dfodd6  48113  dfeven4  48114  dfeven2  48125  dfodd3  48126  dfeven3  48134  dfodd4  48135  dfodd5  48136