Theorem rabeqbidv 3433

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  elfvmptrab1w  7041  elfvmptrab1  7042  fvmptrabfv  7046  elovmporab1w  7689  elovmporab1  7690  ovmpt3rab1  7700  suppval  8203  mpoxopoveq  8261  supeq123d  9466  phival  16970  dfphi2  16977  hashbcval  17206  imasval  17709  ismre  17786  mrisval  17830  isacs  17851  monfval  17933  ismon  17934  monpropd  17938  natfval  18150  isnat  18151  initoval  18194  termoval  18195  gsumvalx  18891  gsumpropd  18893  gsumress  18897  ismgmhm  18911  issubmgm  18917  ismhm  19006  issubm  19024  issubg  19362  isnsg  19391  isgim  19502  isga  19532  cntzfval  19561  isslw  19849  isirred  20676  rnghmval  20697  isrngim  20702  dfrhm2  20731  rhmval0  20732  isrim0  20740  issubrng  20826  issubrg  20850  rrgval  20976  issdrg  21072  abvfval  21094  lssset  21235  islmhm  21329  islmim  21364  islbs  21378  prmidlval  21645  ocvfval  21999  isobs  22053  dsmmval  22067  islinds  22142  mplval  22323  mhpfval  22486  mplbaspropd  22581  dmatval  22834  scmatval  22846  cpmat  23054  cldval  23368  mretopd  23437  neifval  23444  ordtval  23534  ordtbas2  23536  ordtcnv  23546  ordtrest2  23549  cnfval  23578  cnpfval  23579  kgenval  23881  xkoval  23933  dfac14  23964  qtopval  24041  qtopval2  24042  hmeofval  24104  elmptrab  24173  fgval  24216  flimval  24309  utopval  24578  ucnval  24622  iscfilu  24633  ispsmet  24650  ismet  24669  isxmet  24670  blfvalps  24729  cncfval  25236  ishtpy  25320  isphtpy  25329  om1val  25378  cfilfval  25612  caufval  25623  cpnfval  26279  uc1pval  26485  mon1pval  26487  dchrval  27588  leftval  28262  rightval  28263  istrkgl  28947  israg  29199  tgplnfn  29280  plngval  29282  isplng  29283  iseqlg  29439  ttgval  29479  nbgrval  29944  vtxdgfval  30075  vtxdeqd  30085  1egrvtxdg1  30117  umgr2v2evd2  30135  wwlks  30451  wwlksn  30453  wspthsn  30464  wwlksnon  30467  wspthsnon  30468  iswspthsnon  30472  rusgrnumwwlklem  30589  clwwlk  30601  clwwlkn  30644  2clwwlk  30975  numclwlk1lem2  30998  numclwwlkovh0  31000  numclwwlkovq  31002  lnoval  31381  bloval  31410  hmoval  31439  mntoval  33610  tocycval  33736  fxpval  33793  fldgenval  33941  mxidlval  34053  rprmval  34115  minplyval  34404  ordtprsuni  34618  sigagenval  34840  faeval  34946  ismbfm  34951  carsgval  35002  sitgval  35031  reprval  35306  erdszelem3  36124  erdsze  36133  kur14  36147  iscvm  36190  satf  36284  wlimeq12  36758  fwddifval  37104  poimirlem28  38757  istotbnd  38894  isbnd  38905  rngohomval  39089  rngoisoval  39102  idlval  39138  pridlval  39158  maxidlval  39164  igenval  39186  lshpset  40226  lflset  40307  pats  40533  llnset  40753  lplnset  40777  lvolset  40820  lineset  40986  pmapfval  41004  paddfval  41045  lhpset  41243  ldilfset  41356  ltrnfset  41365  ltrnset  41366  dilfsetN  41400  trnfsetN  41403  trnsetN  41404  diaffval  42278  diafval  42279  dicffval  42422  dochffval  42597  lpolsetN  42730  lcdfval  42836  lcdval  42837  mapdffval  42874  mapdfval  42875  prjcrvfval  43858  isnacs  43906  mzpclval  43927  k0004val  45340  dvnprodlem1  47159  fourierdlem2  47322  fourierdlem3  47323  etransclem12  47459  etransclem33  47480  caragenval  47706  smflimlem3  47986  fvmptrab  48565  iccpval  48700  clnbgrval  49123  isisubgr  49163  grtri  49241  stgrfv  49254  gpgov  49343  assintopval  49505  dmatALTval  49715  lcoop  49726  lines  50047  rrxlines  50049  spheres  50061