Theorem rabbiia 3431

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {crab 3427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-rab 3428

This theorem is referenced by:  rabbii  3433  fninfp  7177  fndifnfp  7179  nlimon  7849  dfom2  7866  rankval2  9833  ioopos  13425  prmreclem4  16879  acsfn1  17632  acsfn2  17634  logtayl  26581  ftalem3  26994  ppiub  27124  isuvtx  29195  vtxdginducedm1  29344  finsumvtxdg2size  29351  rgrusgrprc  29390  clwwlknclwwlkdif  29776  numclwwlkqhash  30172  ubthlem1  30667  xpinpreima  33443  xpinpreima2  33444  eulerpartgbij  33928  topdifinfeq  36765  rabimbieq  37658  rmydioph  42357  rmxdioph  42359  expdiophlem2  42365  expdioph  42366  alephiso3  42912  fsovrfovd  43362  k0004val0  43507  nzss  43677  hashnzfz  43680  fourierdlem90  45507  fourierdlem96  45513  fourierdlem97  45514  fourierdlem98  45515  fourierdlem99  45516  fourierdlem100  45517  fourierdlem109  45526  fourierdlem110  45527  fourierdlem112  45529  fourierdlem113  45530  sssmf  46049  dfodd6  46900  dfeven4  46901  dfeven2  46912  dfodd3  46913  dfeven3  46921  dfodd4  46922  dfodd5  46923