Theorem rabeqbidv 3195

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921

This theorem is referenced by:  elfvmptrab1  6305  elovmpt2rab1  6881  ovmpt3rab1  6891  suppval  7297  mpt2xopoveq  7345  supeq123d  8356  phival  15472  dfphi2  15479  hashbcval  15706  imasval  16171  ismre  16250  mrisval  16290  isacs  16312  monfval  16392  ismon  16393  monpropd  16397  natfval  16606  isnat  16607  initoval  16647  termoval  16648  gsumvalx  17270  gsumpropd  17272  gsumress  17276  ismhm  17337  issubm  17347  issubg  17594  isnsg  17623  isgim  17704  isga  17724  cntzfval  17753  isslw  18023  isirred  18699  dfrhm2  18717  isrim0  18723  issubrg  18780  abvfval  18818  lssset  18934  islmhm  19027  islmim  19062  islbs  19076  rrgval  19287  mplval  19428  mplbaspropd  19607  ocvfval  20010  isobs  20064  dsmmval  20078  islinds  20148  dmatval  20298  scmatval  20310  cpmat  20514  cldval  20827  mretopd  20896  neifval  20903  ordtval  20993  ordtbas2  20995  ordtcnv  21005  ordtrest2  21008  cnfval  21037  cnpfval  21038  kgenval  21338  xkoval  21390  dfac14  21421  qtopval  21498  qtopval2  21499  hmeofval  21561  elmptrab  21630  fgval  21674  flimval  21767  utopval  22036  ucnval  22081  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  blfvalps  22188  cncfval  22691  ishtpy  22771  isphtpy  22780  om1val  22830  cfilfval  23062  caufval  23073  cpnfval  23695  uc1pval  23899  mon1pval  23901  dchrval  24959  istrkgl  25357  israg  25592  iseqlg  25747  ttgval  25755  nbgrval  26234  uvtxaval  26287  vtxdgfval  26363  vtxdeqd  26373  1egrvtxdg1  26405  umgr2v2evd2  26423  wwlks  26727  wwlksn  26729  wspthsn  26735  wwlksnon  26738  wspthsnon  26739  iswspthsnon  26741  rusgrnumwwlklem  26865  clwwlks  26879  clwwlksn  26881  numclwwlkovf  27213  numclwwlkovg  27220  numclwwlkovq  27232  numclwwlkovh  27234  lnoval  27607  bloval  27636  hmoval  27665  ordtprsuni  29965  sigagenval  30203  faeval  30309  ismbfm  30314  carsgval  30365  sitgval  30394  reprval  30688  erdszelem3  31175  erdsze  31184  kur14  31198  iscvm  31241  wlimeq12  31765  fwddifval  32269  poimirlem28  33437  istotbnd  33568  isbnd  33579  rngohomval  33763  rngoisoval  33776  idlval  33812  pridlval  33832  maxidlval  33838  igenval  33860  lshpset  34265  lflset  34346  pats  34572  llnset  34791  lplnset  34815  lvolset  34858  lineset  35024  pmapfval  35042  paddfval  35083  lhpset  35281  ldilfset  35394  ltrnfset  35403  ltrnset  35404  dilfsetN  35439  trnfsetN  35442  trnsetN  35443  diaffval  36319  diafval  36320  dicffval  36463  dochffval  36638  lpolsetN  36771  lcdfval  36877  lcdval  36878  mapdffval  36915  mapdfval  36916  isnacs  37267  mzpclval  37288  issdrg  37767  k0004val  38448  fourierdlem2  40326  fourierdlem3  40327  etransclem12  40463  etransclem33  40484  caragenval  40707  smflimlem3  40981  iccpval  41351  ismgmhm  41783  issubmgm  41789  assintopval  41841  rnghmval  41891  isrngisom  41896  dmatALTval  42189  lcoop  42200