Theorem rabbidv 3423

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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3422	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is referenced by:  difeq2  4076  seex  5622  mptiniseg  6242  dfpred3g  6316  elovmporab  7658  elovmpt3rab1  7672  naddcllem  8663  naddov2  8666  naddcom  8670  naddrid  8671  naddass  8684  fineqvlem  9227  mapfien2  9370  supeq1  9406  supeq2  9409  supeq3  9410  oieq1  9475  oieq2  9476  ordtypecbv  9480  ordtypelem3  9483  harval  9523  inf3lema  9594  wemapwe  9667  oef1o  9668  tz9.12lem3  9762  rankvalb  9770  rankvalg  9790  ranksnb  9800  rankonidlem  9801  cardval3  9939  cardidm  9946  alephsuc2  10065  coftr  10258  fin1a2lem11  10395  fin1a2lem12  10396  hsmex  10417  axdc3lem2  10436  zorn2lem1  10481  zorn2lem6  10486  zorn2lem7  10487  zorn2g  10488  wuncval  10728  tskmval  10825  peano5uzti  12687  uzval  12865  rpnnen1  13008  ixxval  13381  fzval  13538  hashbclem  14491  hashbc  14492  shftfn  15112  bitsfval  16482  sadfval  16511  sadcom  16522  smufval  16536  smupp1  16539  smupval  16547  smumullem  16551  gcdval  16555  bezoutlem2  16599  bezoutlem4  16601  lcmval  16651  lcmfval  16680  lcmf0val  16681  lcmfpr  16686  isprm  16732  odzval  16852  pcval  16905  pceulem  16906  pceu  16907  pczpre  16908  pcdiv  16913  prmreclem1  16977  prmreclem4  16980  prmreclem5  16981  ramval  17069  cshws0  17162  imasdsval  17570  mrcval  17667  eldmcoa  18123  chneq1  18669  cycsubg2  19282  cntzval  19392  cntzsnval  19395  odfval  19603  odfvalALT  19604  odval  19605  gexval  19649  efgsfo  19810  dprdval  20076  ablfac1a  20142  ablfac1b  20143  ablfac1eu  20146  ablfaclem1  20158  ablfaclem3  20160  rnghmval  20523  rgspnval  20698  lspval  21077  ocvval  21798  dsmmelbas  21870  frlmsslss  21905  aspval  22003  psrass1lem  22064  psrmulval  22075  mplmonmul  22168  mhpval  22283  mhpmulcl  22293  coe1mul2  22411  pmatcoe1fsupp  22839  istopon  23050  toponsspwpw  23060  clsval  23175  neival  23240  ordtbaslem  23326  ordtbas2  23329  ordtopn1  23332  ordtopn2  23333  cnpval  23374  llyeq  23608  nllyeq  23609  ptfinfin  23657  finlocfin  23658  dissnlocfin  23667  locfindis  23668  xkoopn  23727  kqfval  23861  tsmsfbas  24266  blvalps  24523  blval  24524  nmofval  24852  nmoval  24853  ishtpy  25112  minveclem3b  25568  minveclem3  25569  minveclem4  25572  minveclem5  25573  ovolval  25613  vitalilem2  25749  vitalilem3  25750  vitalilem4  25751  vitali  25753  itg2monolem1  25890  elcpn  26074  mdegmullem  26216  elqaalem1  26461  elqaalem2  26462  elqaalem3  26463  elqaa  26464  aannenlem1  26472  aannenlem2  26473  jensen  27134  vmaval  27258  muval  27277  sgmval  27287  fsumdvdscom  27330  musum  27336  muinv  27338  dchrisum0fval  27650  dchrisum0ff  27652  logsqvma2  27688  pntrlog2bndlem1  27722  cutsval  27954  bdayons  28450  tglngval  28801  plngval  29040  ttgval  29205  ttgitvval  29212  ebtwntg  29313  numedglnl  29475  dfnbgr2  29668  dfnbgr3  29669  uvtxusgr  29733  vtxdgval  29799  rusgrnumwrdl2  29917  iswwlksnon  30183  rusgrnumwwlks  30307  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  clwlknf1oclwwlknlem2  30414  clwwlknon  30422  clwwlk0on0  30424  eupth2  30571  fusgreg2wsplem  30665  fusgreghash2wsp  30670  numclwlk1lem1  30701  sspval  31056  ubthlem1  31203  ubthlem2  31204  ubthlem3  31205  ocval  31613  spanval  31666  chsupid  31745  eigvecval  32229  specval  32231  iunpreima  32890  fcobijfs2  33048  pwrssmgc  33301  fxpgaval  33468  nsgqusf1olem3  33705  selvply1rhmlemb  33890  mplvrpmrhm  33918  psrmonmul  33921  esplyfval  33934  esplyfval0  33935  minplyval  34076  constrsuc  34109  constrcbvlem  34126  crefeq  34216  zarcls1  34240  zarclsun  34241  zarclsiin  34242  zarclsint  34243  zarclssn  34244  zartop  34247  zartopon  34248  zart0  34250  zarmxt1  34251  zarcmp  34253  rhmpreimacnlem  34255  rhmpreimacn  34256  ordtcnvNEW  34291  ordtrest2NEW  34294  ordtconnlem1  34295  measvuni  34585  brfae  34619  omsfval  34665  orvcelval  34840  ballotlemi  34872  bnj602  35284  fineqvnttrclselem2  35516  fineqvnttrclselem3  35517  fineqvnttrclse  35518  onvf1odlem3  35570  subfacp1lem6  35658  kur14  35689  cvmscbv  35731  cvmsi  35738  cvmsval  35739  snmlval  35804  snmlflim  35805  satfv0  35831  satfv1  35836  satfv0fun  35844  satffunlem1lem1  35875  satffunlem2lem1  35877  satfv0fvfmla0  35886  satfv1fvfmla1  35896  prv1n  35904  fvray  36614  fwddifnval  36636  nmulprop  36663  nmulcom  36667  neibastop3  36854  weiunlem  36955  icoreval  37980  fin2so  38239  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  poimirlem32  38284  ftc1anclem6  38330  islinei  40495  pmapval  40512  paddval  40553  paddcom  40568  pclvalN  40645  ldilset  40864  dilsetN  40908  diafval  41786  diaval  41787  docavalN  41878  dicfval  41930  dochfval  42105  dochval  42106  mapdval  42383  mapdsn2  42397  grpods  42942  unitscyglem1  42943  unitscyglem2  42944  unitscyglem3  42945  unitscyglem4  42946  prjcrvval  43347  2rexfrabdioph  43506  3rexfrabdioph  43507  4rexfrabdioph  43508  6rexfrabdioph  43509  7rexfrabdioph  43510  eldioph4i  43522  diophren  43523  pell1qrval  43556  pell14qrval  43558  pell1234qrval  43560  rpnnen3  43742  fnwe2lem1  43760  pwssplit4  43799  pwslnmlem2  43803  dgraaval  43854  itgoval  43871  proot1hash  43905  rp-intrabeq  43931  rp-unirabeq  43932  rfovfvd  44711  rfovfvfvd  44712  rfovcnvf1od  44713  fsovrfovd  44718  fsovfvd  44719  fsovfvfvd  44720  fsovcnvlem  44722  nzss  45010  supminfxr  46161  dvnprodlem1  46643  dvnprodlem2  46644  dvnprodlem3  46645  dvnprod  46646  stoweidlem26  46723  stoweidlem27  46724  stoweidlem31  46728  stoweidlem34  46731  stoweidlem46  46743  fourierdlem79  46882  fourierdlem96  46899  fourierdlem97  46900  fourierdlem98  46901  fourierdlem99  46902  fourierdlem105  46908  fourierdlem107  46910  fourierdlem108  46911  fourierdlem110  46913  etransclem11  46942  salgenval  47018  subsaliuncl  47055  ovnval  47238  ovnval2  47242  ovnval2b  47249  ovncvrrp  47261  ovnsubaddlem1  47267  ovnsubadd  47269  ovncvr2  47308  hspmbl  47326  ovolval2  47341  ovnovollem3  47355  salpreimagelt  47404  salpreimalegt  47406  salpreimagtge  47422  salpreimaltle  47423  issmflem  47424  issmf  47425  salpreimagtlt  47427  smfpreimalt  47428  smfpreimaltf  47433  issmfle  47442  smfpimltxr  47444  smfpreimale  47451  issmfgt  47453  smfpreimagt  47459  issmfge  47467  smflimlem3  47470  smflimlem4  47471  smflim  47474  smfpimgtxr  47477  smfpreimage  47479  fvmptrabdm  48013  elsetpreimafveq  48129  prmdvdsfmtnof1  48322  fppr  48474  dfclnbgr2  48571  dfclnbgr3  48574  dfsclnbgr6  48606  grlimedgclnbgr  48743  grlimgrtri  48751  grilcbri2  48759  bigoval  49312  line  49495  rrxline  49497  sphere  49510  line2y  49518  inpw  49586