Theorem rabeqbidv 3299

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	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	rabeqdv 3298	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3293	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2758	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1596  {crab 3018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rab 3023

This theorem is referenced by:  elfvmptrab1  6419  fvmptrabfv  6423  elovmpt2rab1  6998  ovmpt3rab1  7008  suppval  7417  mpt2xopoveq  7465  supeq123d  8472  phival  15595  dfphi2  15602  hashbcval  15829  imasval  16294  ismre  16373  mrisval  16413  isacs  16434  monfval  16514  ismon  16515  monpropd  16519  natfval  16728  isnat  16729  initoval  16769  termoval  16770  gsumvalx  17392  gsumpropd  17394  gsumress  17398  ismhm  17459  issubm  17469  issubg  17716  isnsg  17745  isgim  17826  isga  17845  cntzfval  17874  isslw  18144  isirred  18820  dfrhm2  18840  isrim0  18846  issubrg  18903  abvfval  18941  lssset  19057  islmhm  19150  islmim  19185  islbs  19199  rrgval  19410  mplval  19551  mplbaspropd  19730  ocvfval  20133  isobs  20187  dsmmval  20201  islinds  20271  dmatval  20421  scmatval  20433  cpmat  20637  cldval  20950  mretopd  21019  neifval  21026  ordtval  21116  ordtbas2  21118  ordtcnv  21128  ordtrest2  21131  cnfval  21160  cnpfval  21161  kgenval  21461  xkoval  21513  dfac14  21544  qtopval  21621  qtopval2  21622  hmeofval  21684  elmptrab  21753  fgval  21796  flimval  21889  utopval  22158  ucnval  22203  iscfilu  22214  ispsmet  22231  ismet  22250  isxmet  22251  blfvalps  22310  cncfval  22813  ishtpy  22893  isphtpy  22902  om1val  22951  cfilfval  23183  caufval  23194  cpnfval  23815  uc1pval  24019  mon1pval  24021  dchrval  25079  istrkgl  25477  israg  25712  iseqlg  25867  ttgval  25875  nbgrval  26349  uvtxavalOLD  26409  vtxdgfval  26494  vtxdeqd  26504  1egrvtxdg1  26536  umgr2v2evd2  26554  wwlks  26859  wwlksn  26861  wspthsn  26873  wwlksnon  26876  wspthsnon  26877  iswspthsnon  26882  iswspthsnonOLD  26883  rusgrnumwwlklem  27013  clwwlk  27027  clwwlkn  27072  clwwlknOLD  27073  2clwwlk  27425  numclwwlkovgOLD  27429  numclwlk1lem2  27452  numclwwlkovh0  27454  numclwwlkovq  27456  numclwwlkovhOLD  27464  lnoval  27837  bloval  27866  hmoval  27895  ordtprsuni  30195  sigagenval  30433  faeval  30539  ismbfm  30544  carsgval  30595  sitgval  30624  reprval  30918  erdszelem3  31403  erdsze  31412  kur14  31426  iscvm  31469  wlimeq12  31991  fwddifval  32496  poimirlem28  33669  istotbnd  33800  isbnd  33811  rngohomval  33995  rngoisoval  34008  idlval  34044  pridlval  34064  maxidlval  34070  igenval  34092  lshpset  34685  lflset  34766  pats  34992  llnset  35211  lplnset  35235  lvolset  35278  lineset  35444  pmapfval  35462  paddfval  35503  lhpset  35701  ldilfset  35814  ltrnfset  35823  ltrnset  35824  dilfsetN  35859  trnfsetN  35862  trnsetN  35863  diaffval  36738  diafval  36739  dicffval  36882  dochffval  37057  lpolsetN  37190  lcdfval  37296  lcdval  37297  mapdffval  37334  mapdfval  37335  isnacs  37686  mzpclval  37707  issdrg  38186  k0004val  38867  fourierdlem2  40746  fourierdlem3  40747  etransclem12  40883  etransclem33  40904  caragenval  41130  smflimlem3  41404  fvmptrab  41733  iccpval  41778  ismgmhm  42210  issubmgm  42216  assintopval  42268  rnghmval  42318  isrngisom  42323  dmatALTval  42616  lcoop  42627