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  7024  elfvmptrab1  7025  fvmptrabfv  7029  elovmporab1w  7655  elovmporab1  7656  ovmpt3rab1  7666  suppval  8150  mpoxopoveq  8206  supeq123d  9447  phival  16702  dfphi2  16709  hashbcval  16937  imasval  17459  ismre  17536  mrisval  17576  isacs  17597  monfval  17681  ismon  17682  monpropd  17686  natfval  17899  isnat  17900  initoval  17945  termoval  17946  gsumvalx  18597  gsumpropd  18599  gsumress  18603  ismhm  18675  issubm  18686  issubg  19008  isnsg  19037  isgim  19138  isga  19157  cntzfval  19186  isslw  19478  isirred  20237  dfrhm2  20257  isrim0OLD  20263  isrim0  20265  issubrg  20323  issdrg  20408  abvfval  20430  lssset  20549  islmhm  20643  islmim  20678  islbs  20692  rrgval  20909  ocvfval  21225  isobs  21281  dsmmval  21295  islinds  21370  mplval  21554  mhpfval  21688  mplbaspropd  21766  dmatval  22001  scmatval  22013  cpmat  22218  cldval  22534  mretopd  22603  neifval  22610  ordtval  22700  ordtbas2  22702  ordtcnv  22712  ordtrest2  22715  cnfval  22744  cnpfval  22745  kgenval  23046  xkoval  23098  dfac14  23129  qtopval  23206  qtopval2  23207  hmeofval  23269  elmptrab  23338  fgval  23381  flimval  23474  utopval  23744  ucnval  23789  iscfilu  23800  ispsmet  23817  ismet  23836  isxmet  23837  blfvalps  23896  cncfval  24411  ishtpy  24495  isphtpy  24504  om1val  24553  cfilfval  24788  caufval  24799  cpnfval  25456  uc1pval  25664  mon1pval  25666  dchrval  26744  leftval  27366  rightval  27367  istrkgl  27747  israg  27986  iseqlg  28156  ttgval  28164  ttgvalOLD  28165  nbgrval  28631  vtxdgfval  28762  vtxdeqd  28772  1egrvtxdg1  28804  umgr2v2evd2  28822  wwlks  29127  wwlksn  29129  wspthsn  29140  wwlksnon  29143  wspthsnon  29144  iswspthsnon  29148  rusgrnumwwlklem  29262  clwwlk  29274  clwwlkn  29317  2clwwlk  29638  numclwlk1lem2  29661  numclwwlkovh0  29663  numclwwlkovq  29665  lnoval  30043  bloval  30072  hmoval  30101  mntoval  32190  tocycval  32308  fldgenval  32443  prmidlval  32600  mxidlval  32622  rprmval  32678  minplyval  32826  ordtprsuni  32968  sigagenval  33207  faeval  33313  ismbfm  33318  carsgval  33371  sitgval  33400  reprval  33691  erdszelem3  34253  erdsze  34262  kur14  34276  iscvm  34319  satf  34413  wlimeq12  34860  fwddifval  35203  poimirlem28  36602  istotbnd  36723  isbnd  36734  rngohomval  36918  rngoisoval  36931  idlval  36967  pridlval  36987  maxidlval  36993  igenval  37015  lshpset  37934  lflset  38015  pats  38241  llnset  38462  lplnset  38486  lvolset  38529  lineset  38695  pmapfval  38713  paddfval  38754  lhpset  38952  ldilfset  39065  ltrnfset  39074  ltrnset  39075  dilfsetN  39109  trnfsetN  39112  trnsetN  39113  diaffval  39987  diafval  39988  dicffval  40131  dochffval  40306  lpolsetN  40439  lcdfval  40545  lcdval  40546  mapdffval  40583  mapdfval  40584  prjcrvfval  41455  isnacs  41524  mzpclval  41545  k0004val  42983  fourierdlem2  44904  fourierdlem3  44905  etransclem12  45041  etransclem33  45062  caragenval  45288  smflimlem3  45568  fvmptrab  46079  iccpval  46162  ismgmhm  46632  issubmgm  46638  assintopval  46694  rnghmval  46768  isrngisom  46773  issubrng  46805  dmatALTval  47159  lcoop  47170  lines  47495  rrxlines  47497  spheres  47510