Theorem rabbiia 3405

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3402

This theorem is referenced by:  rabbii  3406  fninfp  7132  fndifnfp  7134  nlimon  7805  dfom2  7822  rankval2  9744  ioopos  13354  prmreclem4  16861  acsfn1  17598  acsfn2  17600  logtayl  26642  ftalem3  27058  ppiub  27188  isuvtx  29486  vtxdginducedm1  29635  finsumvtxdg2size  29642  rgrusgrprc  29681  clwwlknclwwlkdif  30072  numclwwlkqhash  30468  ubthlem1  30964  psrbasfsupp  33711  xpinpreima  34090  xpinpreima2  34091  eulerpartgbij  34556  rankval2b  35282  fineqvnttrclse  35308  topdifinfeq  37632  rabimbieq  38533  resuppsinopn  42762  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  expdioph  43409  alephiso3  43944  fsovrfovd  44394  k0004val0  44539  nzss  44702  hashnzfz  44705  fourierdlem90  46583  fourierdlem96  46589  fourierdlem97  46590  fourierdlem98  46591  fourierdlem99  46592  fourierdlem100  46593  fourierdlem109  46602  fourierdlem110  46603  fourierdlem112  46605  fourierdlem113  46606  sssmf  47125  dfodd6  48026  dfeven4  48027  dfeven2  48038  dfodd3  48039  dfeven3  48047  dfodd4  48048  dfodd5  48049