Theorem rabeqbidv 3434

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 3432	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  elfvmptrab1w  7012  elfvmptrab1  7013  fvmptrabfv  7017  elovmporab1w  7652  elovmporab1  7653  ovmpt3rab1  7663  suppval  8159  mpoxopoveq  8216  supeq123d  9460  phival  16784  dfphi2  16791  hashbcval  17020  imasval  17523  ismre  17600  mrisval  17640  isacs  17661  monfval  17743  ismon  17744  monpropd  17748  natfval  17960  isnat  17961  initoval  18004  termoval  18005  gsumvalx  18652  gsumpropd  18654  gsumress  18658  ismgmhm  18672  issubmgm  18678  ismhm  18761  issubm  18779  issubg  19107  isnsg  19136  isgim  19243  isga  19272  cntzfval  19301  isslw  19587  isirred  20377  rnghmval  20398  isrngim  20403  dfrhm2  20432  isrim0OLD  20439  isrim0  20441  issubrng  20505  issubrg  20529  rrgval  20655  issdrg  20746  abvfval  20768  lssset  20888  islmhm  20983  islmim  21018  islbs  21032  ocvfval  21624  isobs  21678  dsmmval  21692  islinds  21767  mplval  21947  mhpfval  22074  mplbaspropd  22170  dmatval  22428  scmatval  22440  cpmat  22645  cldval  22959  mretopd  23028  neifval  23035  ordtval  23125  ordtbas2  23127  ordtcnv  23137  ordtrest2  23140  cnfval  23169  cnpfval  23170  kgenval  23471  xkoval  23523  dfac14  23554  qtopval  23631  qtopval2  23632  hmeofval  23694  elmptrab  23763  fgval  23806  flimval  23899  utopval  24169  ucnval  24213  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  blfvalps  24320  cncfval  24830  ishtpy  24920  isphtpy  24929  om1val  24979  cfilfval  25214  caufval  25225  cpnfval  25884  uc1pval  26095  mon1pval  26097  dchrval  27195  leftval  27819  rightval  27820  istrkgl  28383  israg  28622  iseqlg  28792  ttgval  28800  nbgrval  29261  vtxdgfval  29393  vtxdeqd  29403  1egrvtxdg1  29435  umgr2v2evd2  29453  wwlks  29763  wwlksn  29765  wspthsn  29776  wwlksnon  29779  wspthsnon  29780  iswspthsnon  29784  rusgrnumwwlklem  29898  clwwlk  29910  clwwlkn  29953  2clwwlk  30274  numclwlk1lem2  30297  numclwwlkovh0  30299  numclwwlkovq  30301  lnoval  30679  bloval  30708  hmoval  30737  mntoval  32908  tocycval  33065  fldgenval  33252  prmidlval  33398  mxidlval  33422  rprmval  33477  minplyval  33685  ordtprsuni  33896  sigagenval  34117  faeval  34223  ismbfm  34228  carsgval  34281  sitgval  34310  reprval  34588  erdszelem3  35161  erdsze  35170  kur14  35184  iscvm  35227  satf  35321  wlimeq12  35783  fwddifval  36126  poimirlem28  37618  istotbnd  37739  isbnd  37750  rngohomval  37934  rngoisoval  37947  idlval  37983  pridlval  38003  maxidlval  38009  igenval  38031  lshpset  38942  lflset  39023  pats  39249  llnset  39470  lplnset  39494  lvolset  39537  lineset  39703  pmapfval  39721  paddfval  39762  lhpset  39960  ldilfset  40073  ltrnfset  40082  ltrnset  40083  dilfsetN  40117  trnfsetN  40120  trnsetN  40121  diaffval  40995  diafval  40996  dicffval  41139  dochffval  41314  lpolsetN  41447  lcdfval  41553  lcdval  41554  mapdffval  41591  mapdfval  41592  prjcrvfval  42601  isnacs  42674  mzpclval  42695  k0004val  44121  dvnprodlem1  45923  fourierdlem2  46086  fourierdlem3  46087  etransclem12  46223  etransclem33  46244  caragenval  46470  smflimlem3  46750  fvmptrab  47269  iccpval  47377  clnbgrval  47784  isisubgr  47823  grtri  47900  stgrfv  47913  gpgov  47994  assintopval  48128  dmatALTval  48324  lcoop  48335  lines  48659  rrxlines  48661  spheres  48674