Theorem rabeqbidv 3419

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	rabeqbidva 3417	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  elfvmptrab1w  6979  elfvmptrab1  6980  fvmptrabfv  6984  elovmporab1w  7617  elovmporab1  7618  ovmpt3rab1  7628  suppval  8116  mpoxopoveq  8173  supeq123d  9367  phival  16708  dfphi2  16715  hashbcval  16944  imasval  17446  ismre  17523  mrisval  17567  isacs  17588  monfval  17670  ismon  17671  monpropd  17675  natfval  17887  isnat  17888  initoval  17931  termoval  17932  gsumvalx  18615  gsumpropd  18617  gsumress  18621  ismgmhm  18635  issubmgm  18641  ismhm  18724  issubm  18742  issubg  19073  isnsg  19101  isgim  19208  isga  19237  cntzfval  19266  isslw  19554  isirred  20372  rnghmval  20393  isrngim  20398  dfrhm2  20427  isrim0  20435  issubrng  20497  issubrg  20521  rrgval  20647  issdrg  20738  abvfval  20760  lssset  20901  islmhm  20996  islmim  21031  islbs  21045  ocvfval  21638  isobs  21692  dsmmval  21706  islinds  21781  mplval  21961  mhpfval  22098  mplbaspropd  22194  dmatval  22453  scmatval  22465  cpmat  22670  cldval  22984  mretopd  23053  neifval  23060  ordtval  23150  ordtbas2  23152  ordtcnv  23162  ordtrest2  23165  cnfval  23194  cnpfval  23195  kgenval  23496  xkoval  23548  dfac14  23579  qtopval  23656  qtopval2  23657  hmeofval  23719  elmptrab  23788  fgval  23831  flimval  23924  utopval  24193  ucnval  24237  iscfilu  24248  ispsmet  24265  ismet  24284  isxmet  24285  blfvalps  24344  cncfval  24854  ishtpy  24944  isphtpy  24953  om1val  25003  cfilfval  25237  caufval  25248  cpnfval  25907  uc1pval  26118  mon1pval  26120  dchrval  27218  leftval  27862  rightval  27863  istrkgl  28547  israg  28787  iseqlg  28957  ttgval  28965  nbgrval  29427  vtxdgfval  29559  vtxdeqd  29569  1egrvtxdg1  29601  umgr2v2evd2  29619  wwlks  29926  wwlksn  29928  wspthsn  29939  wwlksnon  29942  wspthsnon  29943  iswspthsnon  29947  rusgrnumwwlklem  30064  clwwlk  30076  clwwlkn  30119  2clwwlk  30440  numclwlk1lem2  30463  numclwwlkovh0  30465  numclwwlkovq  30467  lnoval  30846  bloval  30875  hmoval  30904  mntoval  33081  tocycval  33208  fxpval  33265  fldgenval  33412  prmidlval  33536  mxidlval  33560  rprmval  33615  minplyval  33889  ordtprsuni  34103  sigagenval  34324  faeval  34430  ismbfm  34435  carsgval  34487  sitgval  34516  reprval  34794  erdszelem3  35415  erdsze  35424  kur14  35438  iscvm  35481  satf  35575  wlimeq12  36039  fwddifval  36384  poimirlem28  37928  istotbnd  38049  isbnd  38060  rngohomval  38244  rngoisoval  38257  idlval  38293  pridlval  38313  maxidlval  38319  igenval  38341  lshpset  39383  lflset  39464  pats  39690  llnset  39910  lplnset  39934  lvolset  39977  lineset  40143  pmapfval  40161  paddfval  40202  lhpset  40400  ldilfset  40513  ltrnfset  40522  ltrnset  40523  dilfsetN  40557  trnfsetN  40560  trnsetN  40561  diaffval  41435  diafval  41436  dicffval  41579  dochffval  41754  lpolsetN  41887  lcdfval  41993  lcdval  41994  mapdffval  42031  mapdfval  42032  prjcrvfval  43018  isnacs  43090  mzpclval  43111  k0004val  44535  dvnprodlem1  46333  fourierdlem2  46496  fourierdlem3  46497  etransclem12  46633  etransclem33  46654  caragenval  46880  smflimlem3  47160  fvmptrab  47681  iccpval  47804  clnbgrval  48211  isisubgr  48251  grtri  48329  stgrfv  48342  gpgov  48431  assintopval  48594  dmatALTval  48789  lcoop  48800  lines  49120  rrxlines  49122  spheres  49135