Theorem rabbia2 3394

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ⊤wtru 1548   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-rab 3392

This theorem is referenced by:  rabbiia  3395  rabswap  3400  rabeqi  3404  rabrabi  3410  rabrab  3415  f1ossf1o  7070  finsumvtxdg2ssteplem3  29634  clwlknf1oclwwlkn  30172  clwwlknon2x  30191  numclwwlkovh  30461  ballotlem2  34673  fineqvnttrclse  35305  smflim  47220  smflim2  47249  smflimsuplem1  47263  smflimsup  47271  sprvalpwn0  47958