Theorem rabeqbidv 3440

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 group:   𝜑,𝑥

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

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	adantr 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	rabeqbidva 3438	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423

This theorem is referenced by:  elfvmptrab1w  7018  elfvmptrab1  7019  fvmptrabfv  7023  elovmporab1w  7658  elovmporab1  7659  ovmpt3rab1  7669  suppval  8158  mpoxopoveq  8215  supeq123d  9410  phival  16826  dfphi2  16833  hashbcval  17062  imasval  17565  ismre  17642  mrisval  17686  isacs  17707  monfval  17789  ismon  17790  monpropd  17794  natfval  18006  isnat  18007  initoval  18050  termoval  18051  gsumvalx  18734  gsumpropd  18736  gsumress  18740  ismgmhm  18754  issubmgm  18760  ismhm  18843  issubm  18861  issubg  19192  isnsg  19221  isgim  19332  isga  19361  cntzfval  19390  isslw  19678  isirred  20501  rnghmval  20522  isrngim  20527  dfrhm2  20556  isrim0  20564  issubrng  20632  issubrg  20656  rrgval  20782  issdrg  20869  abvfval  20891  lssset  21032  islmhm  21126  islmim  21161  islbs  21175  prmidlval  21433  ocvfval  21785  isobs  21839  dsmmval  21853  islinds  21928  mplval  22107  mhpfval  22270  mplbaspropd  22365  dmatval  22618  scmatval  22630  cpmat  22835  cldval  23149  mretopd  23218  neifval  23225  ordtval  23315  ordtbas2  23317  ordtcnv  23327  ordtrest2  23330  cnfval  23359  cnpfval  23360  kgenval  23661  xkoval  23713  dfac14  23744  qtopval  23821  qtopval2  23822  hmeofval  23884  elmptrab  23953  fgval  23996  flimval  24089  utopval  24358  ucnval  24402  iscfilu  24413  ispsmet  24430  ismet  24449  isxmet  24450  blfvalps  24509  cncfval  25016  ishtpy  25100  isphtpy  25109  om1val  25158  cfilfval  25392  caufval  25403  cpnfval  26060  uc1pval  26266  mon1pval  26268  dchrval  27364  leftval  28008  rightval  28009  istrkgl  28693  israg  28936  tgplnfn  29015  plngval  29017  isplng  29018  iseqlg  29139  ttgval  29165  nbgrval  29627  vtxdgfval  29758  vtxdeqd  29768  1egrvtxdg1  29800  umgr2v2evd2  29818  wwlks  30125  wwlksn  30127  wspthsn  30138  wwlksnon  30141  wspthsnon  30142  iswspthsnon  30146  rusgrnumwwlklem  30263  clwwlk  30275  clwwlkn  30318  2clwwlk  30639  numclwlk1lem2  30662  numclwwlkovh0  30664  numclwwlkovq  30666  lnoval  31045  bloval  31074  hmoval  31103  mntoval  33243  tocycval  33369  fxpval  33426  fldgenval  33576  mxidlval  33689  rprmval  33751  minplyval  34040  ordtprsuni  34254  sigagenval  34475  faeval  34581  ismbfm  34586  carsgval  34638  sitgval  34667  reprval  34942  erdszelem3  35618  erdsze  35627  kur14  35641  iscvm  35684  satf  35778  wlimeq12  36242  fwddifval  36587  poimirlem28  38222  istotbnd  38343  isbnd  38354  rngohomval  38538  rngoisoval  38551  idlval  38587  pridlval  38607  maxidlval  38613  igenval  38635  lshpset  39677  lflset  39758  pats  39984  llnset  40204  lplnset  40228  lvolset  40271  lineset  40437  pmapfval  40455  paddfval  40496  lhpset  40694  ldilfset  40807  ltrnfset  40816  ltrnset  40817  dilfsetN  40851  trnfsetN  40854  trnsetN  40855  diaffval  41729  diafval  41730  dicffval  41873  dochffval  42048  lpolsetN  42181  lcdfval  42287  lcdval  42288  mapdffval  42325  mapdfval  42326  prjcrvfval  43290  isnacs  43362  mzpclval  43383  k0004val  44803  dvnprodlem1  46587  fourierdlem2  46750  fourierdlem3  46751  etransclem12  46887  etransclem33  46908  caragenval  47134  smflimlem3  47414  fvmptrab  47953  iccpval  48088  clnbgrval  48511  isisubgr  48551  grtri  48629  stgrfv  48642  gpgov  48731  assintopval  48894  dmatALTval  49100  lcoop  49111  lines  49431  rrxlines  49433  spheres  49446