Theorem rabbia2 3426

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 3425	. 2 ⊢ (⊤ → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
4	3	mptru 1574	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424

This theorem is referenced by:  rabbiia  3427  rabswap  3432  rabeqi  3436  rabrabi  3442  rabrab  3447  f1ossf1o  7125  finsumvtxdg2ssteplem3  29838  clwlknf1oclwwlkn  30376  clwwlknon2x  30395  numclwwlkovh  30665  ballotlem2  34824  fineqvnttrclse  35460  smflim  47383  smflim2  47412  smflimsuplem1  47426  smflimsup  47434  sprvalpwn0  48121