Theorem rabbia2 3393

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  {crab 3390

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 3391

This theorem is referenced by:  rabbiia  3394  rabswap  3399  rabeqi  3403  rabrabi  3409  rabrab  3414  f1ossf1o  7076  finsumvtxdg2ssteplem3  29634  clwlknf1oclwwlkn  30172  clwwlknon2x  30191  numclwwlkovh  30461  ballotlem2  34652  fineqvnttrclse  35287  smflim  47226  smflim2  47255  smflimsuplem1  47269  smflimsup  47277  sprvalpwn0  47958