Theorem rabbiia 3417

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is used by:  rabbii  3418  fninfp  7179  fndifnfp  7181  nlimon  7862  dfom2  7879  rankval2  9827  rankval2b  9835  ioopos  13555  prmreclem4  17097  acsfn1  17835  acsfn2  17837  logtayl  26988  ftalem3  27402  ppiub  27531  isuvtx  29976  vtxdginducedm1  30124  finsumvtxdg2size  30131  rgrusgrprc  30170  clwwlknclwwlkdif  30570  numclwwlkqhash  30976  ubthlem1  31472  psrbasfsupp  34143  xpinpreima  34538  xpinpreima2  34539  eulerpartgbij  35004  dfscott2  35742  fineqvnttrclse  35792  topdifinfeq  38273  rabimbieq  39185  resuppsinopn  43414  rmydioph  44020  rmxdioph  44022  expdiophlem2  44028  expdioph  44029  alephiso3  44559  fsovrfovd  45008  k0004val0  45153  nzss  45300  hashnzfz  45303  fourierdlem90  47205  fourierdlem96  47211  fourierdlem97  47212  fourierdlem98  47213  fourierdlem99  47214  fourierdlem100  47215  fourierdlem109  47224  fourierdlem110  47225  fourierdlem112  47227  sssmf  47747  dfodd6  48734  dfeven4  48735  dfeven2  48746  dfodd3  48747  dfeven3  48755  dfodd4  48756  dfodd5  48757  dvsec  50855  dvcsc  50856  dvcot  50857