Theorem rabeqbidv 3424

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  elfvmptrab1w  6995  elfvmptrab1  6996  fvmptrabfv  7000  elovmporab1w  7636  elovmporab1  7637  ovmpt3rab1  7647  suppval  8141  mpoxopoveq  8198  supeq123d  9401  phival  16737  dfphi2  16744  hashbcval  16973  imasval  17474  ismre  17551  mrisval  17591  isacs  17612  monfval  17694  ismon  17695  monpropd  17699  natfval  17911  isnat  17912  initoval  17955  termoval  17956  gsumvalx  18603  gsumpropd  18605  gsumress  18609  ismgmhm  18623  issubmgm  18629  ismhm  18712  issubm  18730  issubg  19058  isnsg  19087  isgim  19194  isga  19223  cntzfval  19252  isslw  19538  isirred  20328  rnghmval  20349  isrngim  20354  dfrhm2  20383  isrim0OLD  20390  isrim0  20392  issubrng  20456  issubrg  20480  rrgval  20606  issdrg  20697  abvfval  20719  lssset  20839  islmhm  20934  islmim  20969  islbs  20983  ocvfval  21575  isobs  21629  dsmmval  21643  islinds  21718  mplval  21898  mhpfval  22025  mplbaspropd  22121  dmatval  22379  scmatval  22391  cpmat  22596  cldval  22910  mretopd  22979  neifval  22986  ordtval  23076  ordtbas2  23078  ordtcnv  23088  ordtrest2  23091  cnfval  23120  cnpfval  23121  kgenval  23422  xkoval  23474  dfac14  23505  qtopval  23582  qtopval2  23583  hmeofval  23645  elmptrab  23714  fgval  23757  flimval  23850  utopval  24120  ucnval  24164  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  blfvalps  24271  cncfval  24781  ishtpy  24871  isphtpy  24880  om1val  24930  cfilfval  25164  caufval  25175  cpnfval  25834  uc1pval  26045  mon1pval  26047  dchrval  27145  leftval  27771  rightval  27772  istrkgl  28385  israg  28624  iseqlg  28794  ttgval  28802  nbgrval  29263  vtxdgfval  29395  vtxdeqd  29405  1egrvtxdg1  29437  umgr2v2evd2  29455  wwlks  29765  wwlksn  29767  wspthsn  29778  wwlksnon  29781  wspthsnon  29782  iswspthsnon  29786  rusgrnumwwlklem  29900  clwwlk  29912  clwwlkn  29955  2clwwlk  30276  numclwlk1lem2  30299  numclwwlkovh0  30301  numclwwlkovq  30303  lnoval  30681  bloval  30710  hmoval  30739  mntoval  32908  tocycval  33065  fxpval  33122  fldgenval  33262  prmidlval  33408  mxidlval  33432  rprmval  33487  minplyval  33695  ordtprsuni  33909  sigagenval  34130  faeval  34236  ismbfm  34241  carsgval  34294  sitgval  34323  reprval  34601  erdszelem3  35180  erdsze  35189  kur14  35203  iscvm  35246  satf  35340  wlimeq12  35807  fwddifval  36150  poimirlem28  37642  istotbnd  37763  isbnd  37774  rngohomval  37958  rngoisoval  37971  idlval  38007  pridlval  38027  maxidlval  38033  igenval  38055  lshpset  38971  lflset  39052  pats  39278  llnset  39499  lplnset  39523  lvolset  39566  lineset  39732  pmapfval  39750  paddfval  39791  lhpset  39989  ldilfset  40102  ltrnfset  40111  ltrnset  40112  dilfsetN  40146  trnfsetN  40149  trnsetN  40150  diaffval  41024  diafval  41025  dicffval  41168  dochffval  41343  lpolsetN  41476  lcdfval  41582  lcdval  41583  mapdffval  41620  mapdfval  41621  prjcrvfval  42619  isnacs  42692  mzpclval  42713  k0004val  44139  dvnprodlem1  45944  fourierdlem2  46107  fourierdlem3  46108  etransclem12  46244  etransclem33  46265  caragenval  46491  smflimlem3  46771  fvmptrab  47293  iccpval  47416  clnbgrval  47823  isisubgr  47862  grtri  47939  stgrfv  47952  gpgov  48033  assintopval  48193  dmatALTval  48389  lcoop  48400  lines  48720  rrxlines  48722  spheres  48735