Theorem rabbiia 3409

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3406

This theorem is referenced by:  rabbii  3411  fninfp  7148  fndifnfp  7150  nlimon  7827  dfom2  7844  rankval2  9771  ioopos  13385  prmreclem4  16890  acsfn1  17622  acsfn2  17624  logtayl  26569  ftalem3  26985  ppiub  27115  isuvtx  29322  vtxdginducedm1  29471  finsumvtxdg2size  29478  rgrusgrprc  29517  clwwlknclwwlkdif  29908  numclwwlkqhash  30304  ubthlem1  30799  xpinpreima  33896  xpinpreima2  33897  eulerpartgbij  34363  topdifinfeq  37338  rabimbieq  38240  resuppsinopn  42351  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  alephiso3  43548  fsovrfovd  43998  k0004val0  44143  nzss  44306  hashnzfz  44309  fourierdlem90  46194  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem100  46204  fourierdlem109  46213  fourierdlem110  46214  fourierdlem112  46216  fourierdlem113  46217  sssmf  46736  dfodd6  47638  dfeven4  47639  dfeven2  47650  dfodd3  47651  dfeven3  47659  dfodd4  47660  dfodd5  47661