Theorem rabbidva2 3417

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-rab 3416

This theorem is referenced by:  rabbia2  3418  rabbidva  3422  rabeq  3430  rabeqbidva  3432  extmptsuppeq  8187  dfac2a  10144  hashbclem  14470  n0cutlt  28301  umgrislfupgrlem  29101  wwlksn0s  29843  wwlksnextwrd  29879  wpthswwlks2on  29943  rusgrnumwwlkl1  29950  clwwlknon1  30078  orvcgteel  34500  orvclteel  34505  wevgblacfn  35131  mapdvalc  41648  mapdval4N  41651  ovncvrrp  46593  ovnsubaddlem1  46599  ovnsubadd  46601  ovncvr2  46640  hspmbl  46658  smflim  46806  smflimsuplem1  46849  smflimsuplem3  46851  smflimsuplem7  46855  smflimsup  46857  initopropd  49160  termopropd  49161