Theorem rabbia2 3416

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
rabbia2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))

Assertion

Ref	Expression
rabbia2	⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}

Proof of Theorem rabbia2

Step	Hyp	Ref	Expression
1		rabbia2.1	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))
2	1	a1i 11	. . 3 ⊢ (⊤ → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
3	2	rabbidva2 3415	. 2 ⊢ (⊤ → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
4	3	mptru 1577	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ 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:  rabbiia  3417  rabswap  3422  rabeqi  3426  rabrabi  3431  rabrab  3436  f1ossf1o  7129  finsumvtxdg2ssteplem3  30128  clwlknf1oclwwlkn  30675  clwwlknon2x  30694  numclwwlkovh  30974  ballotlem2  35121  fineqvnttrclse  35792  smflim  47786  smflim2  47815  smflimsuplem1  47829  smflimsup  47837  sprvalpwn0  48564