Theorem rabbiia 3420

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2146  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is used by:  rabbii  3421  fninfp  7189  fndifnfp  7191  nlimon  7872  dfom2  7889  rankval2  9840  rankval2b  9848  ioopos  13568  prmreclem4  17112  acsfn1  17850  acsfn2  17852  logtayl  27003  ftalem3  27417  ppiub  27546  isuvtx  29991  vtxdginducedm1  30139  finsumvtxdg2size  30146  rgrusgrprc  30185  clwwlknclwwlkdif  30585  numclwwlkqhash  30991  ubthlem1  31487  psrbasfsupp  34199  xpinpreima  34594  xpinpreima2  34595  eulerpartgbij  35060  dfscott2  35808  fineqvnttrclse  35866  topdifinfeq  38416  rabimbieq  39328  resuppsinopn  43557  rmydioph  44164  rmxdioph  44166  expdiophlem2  44172  expdioph  44173  alephiso3  44703  fsovrfovd  45152  k0004val0  45297  nzss  45444  hashnzfz  45447  fourierdlem90  47348  fourierdlem96  47354  fourierdlem97  47355  fourierdlem98  47356  fourierdlem99  47357  fourierdlem100  47358  fourierdlem109  47367  fourierdlem110  47368  fourierdlem112  47370  sssmf  47890  dfodd6  48877  dfeven4  48878  dfeven2  48889  dfodd3  48890  dfeven3  48898  dfodd4  48899  dfodd5  48900  dvsec  51073  dvcsc  51074  dvcot  51075