Theorem rabeqbidv 3449

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433

This theorem is referenced by:  elfvmptrab1w  7011  elfvmptrab1  7012  fvmptrabfv  7016  elovmporab1w  7637  elovmporab1  7638  ovmpt3rab1  7648  suppval  8132  mpoxopoveq  8188  supeq123d  9429  phival  16684  dfphi2  16691  hashbcval  16919  imasval  17441  ismre  17518  mrisval  17558  isacs  17579  monfval  17663  ismon  17664  monpropd  17668  natfval  17881  isnat  17882  initoval  17927  termoval  17928  gsumvalx  18579  gsumpropd  18581  gsumress  18585  ismhm  18651  issubm  18662  issubg  18980  isnsg  19009  isgim  19104  isga  19123  cntzfval  19152  isslw  19442  isirred  20185  dfrhm2  20205  isrim0OLD  20211  isrim0  20213  issubrg  20314  issdrg  20355  abvfval  20377  lssset  20495  islmhm  20589  islmim  20624  islbs  20638  rrgval  20841  ocvfval  21154  isobs  21210  dsmmval  21224  islinds  21299  mplval  21481  mhpfval  21613  mplbaspropd  21692  dmatval  21925  scmatval  21937  cpmat  22142  cldval  22458  mretopd  22527  neifval  22534  ordtval  22624  ordtbas2  22626  ordtcnv  22636  ordtrest2  22639  cnfval  22668  cnpfval  22669  kgenval  22970  xkoval  23022  dfac14  23053  qtopval  23130  qtopval2  23131  hmeofval  23193  elmptrab  23262  fgval  23305  flimval  23398  utopval  23668  ucnval  23713  iscfilu  23724  ispsmet  23741  ismet  23760  isxmet  23761  blfvalps  23820  cncfval  24335  ishtpy  24419  isphtpy  24428  om1val  24477  cfilfval  24712  caufval  24723  cpnfval  25380  uc1pval  25588  mon1pval  25590  dchrval  26666  leftval  27287  rightval  27288  istrkgl  27638  israg  27877  iseqlg  28047  ttgval  28055  ttgvalOLD  28056  nbgrval  28522  vtxdgfval  28653  vtxdeqd  28663  1egrvtxdg1  28695  umgr2v2evd2  28713  wwlks  29018  wwlksn  29020  wspthsn  29031  wwlksnon  29034  wspthsnon  29035  iswspthsnon  29039  rusgrnumwwlklem  29153  clwwlk  29165  clwwlkn  29208  2clwwlk  29529  numclwlk1lem2  29552  numclwwlkovh0  29554  numclwwlkovq  29556  lnoval  29932  bloval  29961  hmoval  29990  mntoval  32087  tocycval  32202  fldgenval  32328  prmidlval  32470  mxidlval  32492  rprmval  32542  minplyval  32666  ordtprsuni  32794  sigagenval  33033  faeval  33139  ismbfm  33144  carsgval  33197  sitgval  33226  reprval  33517  erdszelem3  34079  erdsze  34088  kur14  34102  iscvm  34145  satf  34239  wlimeq12  34685  fwddifval  35028  poimirlem28  36384  istotbnd  36506  isbnd  36517  rngohomval  36701  rngoisoval  36714  idlval  36750  pridlval  36770  maxidlval  36776  igenval  36798  lshpset  37717  lflset  37798  pats  38024  llnset  38245  lplnset  38269  lvolset  38312  lineset  38478  pmapfval  38496  paddfval  38537  lhpset  38735  ldilfset  38848  ltrnfset  38857  ltrnset  38858  dilfsetN  38892  trnfsetN  38895  trnsetN  38896  diaffval  39770  diafval  39771  dicffval  39914  dochffval  40089  lpolsetN  40222  lcdfval  40328  lcdval  40329  mapdffval  40366  mapdfval  40367  prjcrvfval  41219  isnacs  41277  mzpclval  41298  k0004val  42736  fourierdlem2  44662  fourierdlem3  44663  etransclem12  44799  etransclem33  44820  caragenval  45046  smflimlem3  45326  fvmptrab  45836  iccpval  45919  ismgmhm  46389  issubmgm  46395  assintopval  46451  rnghmval  46501  isrngisom  46506  dmatALTval  46793  lcoop  46804  lines  47129  rrxlines  47131  spheres  47144