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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  {cab 2741  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-rab 3416

This theorem is used by:  rabbia2  3418  rabbidva  3421  rabeq  3429  rabeqbidva  3431  rabsneq  4602  extmptsuppeq  8216  dfac2a  10218  hashbclem  14607  n0cutlt  28757  umgrislfupgrlem  29712  wwlksn0s  30462  wwlksnextwrd  30498  wpthswwlks2on  30565  rusgrnumwwlkl1  30572  clwwlknon1  30700  orvcgteel  35153  orvclteel  35158  wevgblacfn  35993  mapdvalc  42826  mapdval4N  42829  ovncvrrp  47713  ovnsubaddlem1  47719  ovnsubadd  47721  ovncvr2  47760  hspmbl  47778  smflim  47926  smflimsuplem1  47969  smflimsuplem3  47971  smflimsuplem7  47975  smflimsup  47977  initopropd  50504  termopropd  50505