Theorem rabbidva2 3401

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)

Hypothesis

Ref	Expression
rabbidva2.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))

Assertion

Ref	Expression
rabbidva2	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem rabbidva2

Step	Hyp	Ref	Expression
1		rabbidva2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	abbidv 2802	. 2 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)})
3		df-rab 3400	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 3400	. 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)}
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  rabbia2  3402  rabbidva  3405  rabeq  3413  rabeqbidva  3415  extmptsuppeq  8130  dfac2a  10040  hashbclem  14375  n0cutlt  28355  umgrislfupgrlem  29195  wwlksn0s  29934  wwlksnextwrd  29970  wpthswwlks2on  30037  rusgrnumwwlkl1  30044  clwwlknon1  30172  orvcgteel  34625  orvclteel  34630  wevgblacfn  35303  mapdvalc  41899  mapdval4N  41902  ovncvrrp  46818  ovnsubaddlem1  46824  ovnsubadd  46826  ovncvr2  46865  hspmbl  46883  smflim  47031  smflimsuplem1  47074  smflimsuplem3  47076  smflimsuplem7  47080  smflimsup  47082  initopropd  49498  termopropd  49499