Theorem rabbiia 3416

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  rabbii  3417  fninfp  7173  fndifnfp  7175  nlimon  7848  dfom2  7865  rankval2  9803  ioopos  13480  prmreclem4  17014  acsfn1  17752  acsfn2  17754  logtayl  26900  ftalem3  27314  ppiub  27443  isuvtx  29858  vtxdginducedm1  30006  finsumvtxdg2size  30013  rgrusgrprc  30052  clwwlknclwwlkdif  30452  numclwwlkqhash  30858  ubthlem1  31354  psrbasfsupp  34024  xpinpreima  34419  xpinpreima2  34420  eulerpartgbij  34886  rankval2b  35609  dfscott2  35628  fineqvnttrclse  35653  topdifinfeq  38107  rabimbieq  39004  resuppsinopn  43241  rmydioph  43858  rmxdioph  43860  expdiophlem2  43866  expdioph  43867  alephiso3  44402  fsovrfovd  44852  k0004val0  44997  nzss  45144  hashnzfz  45147  fourierdlem90  47027  fourierdlem96  47033  fourierdlem97  47034  fourierdlem98  47035  fourierdlem99  47036  fourierdlem100  47037  fourierdlem109  47046  fourierdlem110  47047  fourierdlem112  47049  sssmf  47569  dfodd6  48556  dfeven4  48557  dfeven2  48568  dfodd3  48569  dfeven3  48577  dfodd4  48578  dfodd5  48579  dvsec  50692  dvcsc  50693  dvcot  50694