Theorem rabeqbidv 2794

Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)

Hypotheses

Ref	Expression
rabeqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
rabeqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

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

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeq 2791	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 14	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
4		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
5	4	rabbidv 2788	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
6	3, 5	eqtrd 2262	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  {crab 2512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rab 2517

This theorem is referenced by:  elfvmptrab1  5731  elovmporab1w  6212  mpoxopoveq  6392  supeq123d  7169  phival  12751  dfphi2  12758  gsumress  13444  ismhm  13510  mhmex  13511  issubm  13521  issubg  13726  subgex  13729  isnsg  13755  dfrhm2  14134  isrim0  14141  issubrng  14179  issubrg  14201  rrgval  14242  lsssetm  14336  mplvalcoe  14670  cldval  14789  neifval  14830  cnfval  14884  cnpfval  14885  cnprcl2k  14896  hmeofvalg  14993  ispsmet  15013  ismet  15034  isxmet  15035  blfvalps  15075  cncfval  15262  vtxdgfval  16048  vtxdgop  16052  vtxdeqd  16056  clwwlkg  16136  clwwlkng  16148