Theorem rabbidva2 3405

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 2805	. 2 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)})
3		df-rab 3404	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 3404	. 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)}
5	2, 3, 4	3eqtr4g 2801	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  {cab 2713  {crab 3403

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-rab 3404

This theorem is referenced by:  rabbia2  3406  rabbidva  3410  rabeq  3417  extmptsuppeq  8074  dfac2a  9986  hashbclem  14264  umgrislfupgrlem  27781  wwlksn0s  28514  wwlksnextwrd  28550  wpthswwlks2on  28614  rusgrnumwwlkl1  28621  clwwlknon1  28749  orvcgteel  32734  orvclteel  32739  mapdvalc  39897  mapdval4N  39900  ovncvrrp  44439  ovnsubaddlem1  44445  ovnsubadd  44447  ovncvr2  44486  hspmbl  44504  smflim  44652  smflimsuplem1  44695  smflimsuplem3  44697  smflimsuplem7  44701  smflimsup  44703