Theorem rabeqbidv 3408

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	1	rabeqdv 3407	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3403	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2814	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  {crab 3092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-ral 3093  df-rab 3097

This theorem is referenced by:  elfvmptrab1  6620  fvmptrabfv  6624  elovmporab1  7211  ovmpt3rab1  7221  suppval  7635  mpoxopoveq  7688  supeq123d  8709  phival  15960  dfphi2  15967  hashbcval  16194  imasval  16640  ismre  16719  mrisval  16759  isacs  16780  monfval  16860  ismon  16861  monpropd  16865  natfval  17074  isnat  17075  initoval  17115  termoval  17116  gsumvalx  17738  gsumpropd  17740  gsumress  17744  ismhm  17805  issubm  17815  issubg  18063  isnsg  18092  isgim  18173  isga  18192  cntzfval  18221  isslw  18494  isirred  19172  dfrhm2  19192  isrim0  19198  issubrg  19258  issdrg  19296  abvfval  19311  lssset  19427  islmhm  19521  islmim  19556  islbs  19570  rrgval  19781  mplval  19922  mhpfval  20038  mplbaspropd  20108  ocvfval  20512  isobs  20566  dsmmval  20580  islinds  20655  dmatval  20805  scmatval  20817  cpmat  21021  cldval  21335  mretopd  21404  neifval  21411  ordtval  21501  ordtbas2  21503  ordtcnv  21513  ordtrest2  21516  cnfval  21545  cnpfval  21546  kgenval  21847  xkoval  21899  dfac14  21930  qtopval  22007  qtopval2  22008  hmeofval  22070  elmptrab  22139  fgval  22182  flimval  22275  utopval  22544  ucnval  22589  iscfilu  22600  ispsmet  22617  ismet  22636  isxmet  22637  blfvalps  22696  cncfval  23199  ishtpy  23279  isphtpy  23288  om1val  23337  cfilfval  23570  caufval  23581  cpnfval  24232  uc1pval  24436  mon1pval  24438  dchrval  25512  istrkgl  25946  israg  26185  iseqlg  26356  ttgval  26364  nbgrval  26821  vtxdgfval  26952  vtxdeqd  26962  1egrvtxdg1  26994  umgr2v2evd2  27012  wwlks  27321  wwlksn  27323  wspthsn  27334  wwlksnon  27337  wspthsnon  27338  iswspthsnon  27342  rusgrnumwwlklem  27476  clwwlk  27489  clwwlkn  27541  2clwwlk  27884  numclwlk1lem2  27923  numclwwlkovh0  27925  numclwwlkovq  27927  lnoval  28306  bloval  28335  hmoval  28364  tocycval  30452  ordtprsuni  30812  sigagenval  31050  faeval  31156  ismbfm  31161  carsgval  31212  sitgval  31241  reprval  31535  erdszelem3  32031  erdsze  32040  kur14  32054  iscvm  32097  satf  32187  wlimeq12  32633  fwddifval  33150  poimirlem28  34367  istotbnd  34495  isbnd  34506  rngohomval  34690  rngoisoval  34703  idlval  34739  pridlval  34759  maxidlval  34765  igenval  34787  lshpset  35565  lflset  35646  pats  35872  llnset  36092  lplnset  36116  lvolset  36159  lineset  36325  pmapfval  36343  paddfval  36384  lhpset  36582  ldilfset  36695  ltrnfset  36704  ltrnset  36705  dilfsetN  36739  trnfsetN  36742  trnsetN  36743  diaffval  37617  diafval  37618  dicffval  37761  dochffval  37936  lpolsetN  38069  lcdfval  38175  lcdval  38176  mapdffval  38213  mapdfval  38214  isnacs  38702  mzpclval  38723  k0004val  39869  fourierdlem2  41831  fourierdlem3  41832  etransclem12  41968  etransclem33  41989  caragenval  42212  smflimlem3  42486  fvmptrab  42903  iccpval  42953  ismgmhm  43424  issubmgm  43430  assintopval  43482  rnghmval  43532  isrngisom  43537  dmatALTval  43828  lcoop  43839  lines  44092  rrxlines  44094  spheres  44107