Theorem rabbiia 3405

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3402

This theorem is referenced by:  rabbii  3406  fninfp  7130  fndifnfp  7132  nlimon  7803  dfom2  7820  rankval2  9742  ioopos  13352  prmreclem4  16859  acsfn1  17596  acsfn2  17598  logtayl  26640  ftalem3  27056  ppiub  27186  isuvtx  29484  vtxdginducedm1  29633  finsumvtxdg2size  29640  rgrusgrprc  29679  clwwlknclwwlkdif  30070  numclwwlkqhash  30466  ubthlem1  30962  psrbasfsupp  33709  xpinpreima  34088  xpinpreima2  34089  eulerpartgbij  34554  rankval2b  35280  fineqvnttrclse  35306  topdifinfeq  37609  rabimbieq  38508  resuppsinopn  42737  rmydioph  43375  rmxdioph  43377  expdiophlem2  43383  expdioph  43384  alephiso3  43919  fsovrfovd  44369  k0004val0  44514  nzss  44677  hashnzfz  44680  fourierdlem90  46558  fourierdlem96  46564  fourierdlem97  46565  fourierdlem98  46566  fourierdlem99  46567  fourierdlem100  46568  fourierdlem109  46577  fourierdlem110  46578  fourierdlem112  46580  fourierdlem113  46581  sssmf  47100  dfodd6  48001  dfeven4  48002  dfeven2  48013  dfodd3  48014  dfeven3  48022  dfodd4  48023  dfodd5  48024