Theorem rabbidv 3420

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)

Hypothesis

Ref	Expression
rabbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3419	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is referenced by:  difeq2  4074  seex  5604  mptiniseg  6222  dfpred3g  6296  elovmporab  7638  elovmpt3rab1  7652  naddcllem  8641  naddov2  8644  naddcom  8648  naddrid  8649  naddass  8662  fineqvlem  9206  mapfien2  9352  supeq1  9388  supeq2  9391  supeq3  9392  oieq1  9457  oieq2  9458  ordtypecbv  9462  ordtypelem3  9465  harval  9505  inf3lema  9576  wemapwe  9649  oef1o  9650  tz9.12lem3  9744  rankvalb  9752  rankvalg  9772  ranksnb  9782  rankonidlem  9783  cardval3  9907  cardidm  9914  alephsuc2  10033  coftr  10227  fin1a2lem11  10364  fin1a2lem12  10365  hsmex  10386  axdc3lem2  10405  zorn2lem1  10450  zorn2lem6  10455  zorn2lem7  10456  zorn2g  10457  wuncval  10697  tskmval  10794  peano5uzti  12660  uzval  12838  rpnnen1  12981  ixxval  13354  fzval  13511  hashbclem  14462  hashbc  14463  shftfn  15083  bitsfval  16440  sadfval  16469  sadcom  16480  smufval  16494  smupp1  16497  smupval  16505  smumullem  16509  gcdval  16513  bezoutlem2  16557  bezoutlem4  16559  lcmval  16609  lcmfval  16638  lcmf0val  16639  lcmfpr  16644  isprm  16690  odzval  16810  pcval  16863  pceulem  16864  pceu  16865  pczpre  16866  pcdiv  16871  prmreclem1  16935  prmreclem4  16938  prmreclem5  16939  ramval  17027  cshws0  17120  imasdsval  17528  mrcval  17625  eldmcoa  18081  chneq1  18627  cycsubg2  19234  cntzval  19344  cntzsnval  19347  odfval  19555  odfvalALT  19556  odval  19557  gexval  19601  efgsfo  19762  dprdval  20028  ablfac1a  20094  ablfac1b  20095  ablfac1eu  20098  ablfaclem1  20110  ablfaclem3  20112  rnghmval  20468  rgspnval  20641  lspval  21022  ocvval  21699  dsmmelbas  21771  frlmsslss  21806  aspval  21904  psrass1lem  21965  psrmulval  21976  mplmonmul  22069  mhpval  22184  mhpmulcl  22194  coe1mul2  22312  pmatcoe1fsupp  22741  istopon  22952  toponsspwpw  22962  clsval  23077  neival  23142  ordtbaslem  23228  ordtbas2  23231  ordtopn1  23234  ordtopn2  23235  cnpval  23276  llyeq  23510  nllyeq  23511  ptfinfin  23559  finlocfin  23560  dissnlocfin  23569  locfindis  23570  xkoopn  23629  kqfval  23763  tsmsfbas  24168  blvalps  24425  blval  24426  nmofval  24754  nmoval  24755  ishtpy  25014  minveclem3b  25470  minveclem3  25471  minveclem4  25474  minveclem5  25475  ovolval  25515  vitalilem2  25651  vitalilem3  25652  vitalilem4  25653  vitali  25655  itg2monolem1  25792  elcpn  25976  mdegmullem  26118  elqaalem1  26360  elqaalem2  26361  elqaalem3  26362  elqaa  26363  aannenlem1  26369  aannenlem2  26370  jensen  27030  vmaval  27154  muval  27173  sgmval  27183  fsumdvdscom  27226  musum  27232  muinv  27234  dchrisum0fval  27546  dchrisum0ff  27548  logsqvma2  27584  pntrlog2bndlem1  27618  cutsval  27850  bdayons  28346  tglngval  28697  ttgval  29021  ttgitvval  29028  ebtwntg  29129  numedglnl  29291  dfnbgr2  29484  dfnbgr3  29485  uvtxusgr  29549  vtxdgval  29615  rusgrnumwrdl2  29733  iswwlksnon  29999  rusgrnumwwlks  30123  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  clwlknf1oclwwlknlem2  30230  clwwlknon  30238  clwwlk0on0  30240  eupth2  30387  fusgreg2wsplem  30481  fusgreghash2wsp  30486  numclwlk1lem1  30517  sspval  30872  ubthlem1  31019  ubthlem2  31020  ubthlem3  31021  ocval  31429  spanval  31482  chsupid  31561  eigvecval  32045  specval  32047  iunpreima  32713  fcobijfs2  32874  pwrssmgc  33139  fxpgaval  33308  nsgqusf1olem3  33562  selvply1rhmlemb  33777  mplvrpmrhm  33805  psrmonmul  33808  esplyfval  33821  esplyfval0  33822  minplyval  33963  constrsuc  33996  constrcbvlem  34013  crefeq  34103  zarcls1  34127  zarclsun  34128  zarclsiin  34129  zarclsint  34130  zarclssn  34131  zartop  34134  zartopon  34135  zart0  34137  zarmxt1  34138  zarcmp  34140  rhmpreimacnlem  34142  rhmpreimacn  34143  ordtcnvNEW  34178  ordtrest2NEW  34181  ordtconnlem1  34182  measvuni  34472  brfae  34506  omsfval  34552  orvcelval  34727  ballotlemi  34759  bnj602  35174  fineqvnttrclselem2  35382  fineqvnttrclselem3  35383  fineqvnttrclse  35384  onvf1odlem3  35412  subfacp1lem6  35499  kur14  35530  cvmscbv  35572  cvmsi  35579  cvmsval  35580  snmlval  35645  snmlflim  35646  satfv0  35672  satfv1  35677  satfv0fun  35685  satffunlem1lem1  35716  satffunlem2lem1  35718  satfv0fvfmla0  35727  satfv1fvfmla1  35737  prv1n  35745  fvray  36455  fwddifnval  36477  nmulprop  36504  nmulcom  36508  neibastop3  36686  weiunlem  36787  icoreval  37811  fin2so  38070  poimirlem26  38109  poimirlem27  38110  poimirlem28  38111  poimirlem32  38115  ftc1anclem6  38161  islinei  40328  pmapval  40345  paddval  40386  paddcom  40401  pclvalN  40478  ldilset  40697  dilsetN  40741  diafval  41619  diaval  41620  docavalN  41711  dicfval  41763  dochfval  41938  dochval  41939  mapdval  42216  mapdsn2  42230  grpods  42775  unitscyglem1  42776  unitscyglem2  42777  unitscyglem3  42778  unitscyglem4  42779  prjcrvval  43178  2rexfrabdioph  43337  3rexfrabdioph  43338  4rexfrabdioph  43339  6rexfrabdioph  43340  7rexfrabdioph  43341  eldioph4i  43353  diophren  43354  pell1qrval  43387  pell14qrval  43389  pell1234qrval  43391  rpnnen3  43573  fnwe2lem1  43591  pwssplit4  43630  pwslnmlem2  43634  dgraaval  43685  itgoval  43702  proot1hash  43736  rp-intrabeq  43762  rp-unirabeq  43763  rfovfvd  44542  rfovfvfvd  44543  rfovcnvf1od  44544  fsovrfovd  44549  fsovfvd  44550  fsovfvfvd  44551  fsovcnvlem  44553  nzss  44857  supminfxr  46002  dvnprodlem1  46484  dvnprodlem2  46485  dvnprodlem3  46486  dvnprod  46487  stoweidlem26  46564  stoweidlem27  46565  stoweidlem31  46569  stoweidlem34  46572  stoweidlem46  46584  fourierdlem79  46723  fourierdlem96  46740  fourierdlem97  46741  fourierdlem98  46742  fourierdlem99  46743  fourierdlem105  46749  fourierdlem107  46751  fourierdlem108  46752  fourierdlem110  46754  etransclem11  46783  salgenval  46859  subsaliuncl  46896  ovnval  47079  ovnval2  47083  ovnval2b  47090  ovncvrrp  47102  ovnsubaddlem1  47108  ovnsubadd  47110  ovncvr2  47149  hspmbl  47167  ovolval2  47182  ovnovollem3  47196  salpreimagelt  47245  salpreimalegt  47247  salpreimagtge  47263  salpreimaltle  47264  issmflem  47265  issmf  47266  salpreimagtlt  47268  smfpreimalt  47269  smfpreimaltf  47274  issmfle  47283  smfpimltxr  47285  smfpreimale  47292  issmfgt  47294  smfpreimagt  47300  issmfge  47308  smflimlem3  47311  smflimlem4  47312  smflim  47315  smfpimgtxr  47318  smfpreimage  47320  fvmptrabdm  47851  elsetpreimafveq  47967  prmdvdsfmtnof1  48160  fppr  48312  dfclnbgr2  48409  dfclnbgr3  48412  dfsclnbgr6  48444  grlimedgclnbgr  48581  grlimgrtri  48589  grilcbri2  48597  bigoval  49135  line  49318  rrxline  49320  sphere  49333  line2y  49341  inpw  49410