Theorem rabbidv 3433

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-rab 3426

This theorem is referenced by:  difeq2  4103  seex  5622  mptiniseg  6218  dfpred3g  6292  elovmporab  7626  elovmpt3rab1  7640  naddcllem  8649  naddov2  8652  naddcom  8655  naddrid  8656  naddass  8669  fineqvlem  9235  mapfien2  9376  supeq1  9412  supeq2  9415  supeq3  9416  oieq1  9479  oieq2  9480  ordtypecbv  9484  ordtypelem3  9487  harval  9527  inf3lema  9591  wemapwe  9664  oef1o  9665  tz9.12lem3  9756  rankvalb  9764  rankvalg  9784  ranksnb  9794  rankonidlem  9795  cardval3  9919  cardidm  9926  alephsuc2  10047  coftr  10240  fin1a2lem11  10377  fin1a2lem12  10378  hsmex  10399  axdc3lem2  10418  zorn2lem1  10463  zorn2lem6  10468  zorn2lem7  10469  zorn2g  10470  wuncval  10709  tskmval  10806  peano5uzti  12624  uzval  12796  rpnnen1  12939  ixxval  13304  fzval  13458  hashbclem  14383  hashbc  14384  shftfn  14992  bitsfval  16336  sadfval  16365  sadcom  16376  smufval  16390  smupp1  16393  smupval  16401  smumullem  16405  gcdval  16409  bezoutlem2  16454  bezoutlem4  16456  lcmval  16501  lcmfval  16530  lcmf0val  16531  lcmfpr  16536  isprm  16582  odzval  16696  pcval  16749  pceulem  16750  pceu  16751  pczpre  16752  pcdiv  16757  prmreclem1  16821  prmreclem4  16824  prmreclem5  16825  ramval  16913  cshws0  17007  imasdsval  17433  mrcval  17526  eldmcoa  17987  cycsubg2  19039  cntzval  19137  cntzsnval  19140  odfval  19350  odfvalALT  19351  odval  19352  gexval  19396  efgsfo  19557  dprdval  19818  ablfac1a  19884  ablfac1b  19885  ablfac1eu  19888  ablfaclem1  19900  ablfaclem3  19902  lspval  20515  ocvval  21130  dsmmelbas  21204  frlmsslss  21239  aspval  21335  psrass1lemOLD  21401  psrass1lem  21404  psrmulval  21413  mplmonmul  21496  mhpval  21589  mhpmulcl  21598  coe1mul2  21699  pmatcoe1fsupp  22109  istopon  22320  toponsspwpw  22330  clsval  22447  neival  22512  ordtbaslem  22598  ordtbas2  22601  ordtopn1  22604  ordtopn2  22605  cnpval  22646  llyeq  22880  nllyeq  22881  ptfinfin  22929  finlocfin  22930  dissnlocfin  22939  locfindis  22940  xkoopn  22999  kqfval  23133  tsmsfbas  23538  blvalps  23797  blval  23798  nmofval  24137  nmoval  24138  ishtpy  24394  minveclem3b  24851  minveclem3  24852  minveclem4  24855  minveclem5  24856  ovolval  24896  vitalilem2  25032  vitalilem3  25033  vitalilem4  25034  vitali  25036  itg2monolem1  25174  elcpn  25357  mdegmullem  25502  elqaalem1  25738  elqaalem2  25739  elqaalem3  25740  elqaa  25741  aannenlem1  25747  aannenlem2  25748  jensen  26397  vmaval  26521  muval  26540  sgmval  26550  fsumdvdscom  26593  musum  26599  muinv  26601  dchrisum0fval  26912  dchrisum0ff  26914  logsqvma2  26950  pntrlog2bndlem1  26984  scutval  27204  tglngval  27597  ttgval  27921  ttgvalOLD  27922  ttgitvval  27934  ebtwntg  28035  numedglnl  28199  dfnbgr2  28389  dfnbgr3  28390  uvtxusgr  28454  vtxdgval  28520  rusgrnumwrdl2  28638  iswwlksnon  28902  rusgrnumwwlks  29023  hashecclwwlkn1  29125  umgrhashecclwwlk  29126  clwlknf1oclwwlknlem2  29130  clwwlknon  29138  clwwlk0on0  29140  eupth2  29287  fusgreg2wsplem  29381  fusgreghash2wsp  29386  numclwlk1lem1  29417  sspval  29769  ubthlem1  29916  ubthlem2  29917  ubthlem3  29918  ocval  30326  spanval  30379  chsupid  30458  eigvecval  30942  specval  30944  iunpreima  31591  pwrssmgc  31971  nsgqusf1olem3  32308  minplyval  32502  crefeq  32556  zarcls1  32580  zarclsun  32581  zarclsiin  32582  zarclsint  32583  zarclssn  32584  zartop  32587  zartopon  32588  zart0  32590  zarmxt1  32591  zarcmp  32593  rhmpreimacnlem  32595  rhmpreimacn  32596  ordtcnvNEW  32631  ordtrest2NEW  32634  ordtconnlem1  32635  measvuni  32943  brfae  32977  omsfval  33024  orvcelval  33198  ballotlemi  33230  bnj602  33657  subfacp1lem6  33907  kur14  33938  cvmscbv  33980  cvmsi  33987  cvmsval  33988  snmlval  34053  snmlflim  34054  satfv0  34080  satfv1  34085  satfv0fun  34093  satffunlem1lem1  34124  satffunlem2lem1  34126  satfv0fvfmla0  34135  satfv1fvfmla1  34145  prv1n  34153  fvray  34843  fwddifnval  34865  neibastop3  34951  icoreval  35938  fin2so  36179  poimirlem26  36218  poimirlem27  36219  poimirlem28  36220  poimirlem32  36224  ftc1anclem6  36270  islinei  38316  pmapval  38333  paddval  38374  paddcom  38389  pclvalN  38466  ldilset  38685  dilsetN  38729  diafval  39607  diaval  39608  docavalN  39699  dicfval  39751  dochfval  39926  dochval  39927  mapdval  40204  mapdsn2  40218  prjcrvval  41068  2rexfrabdioph  41217  3rexfrabdioph  41218  4rexfrabdioph  41219  6rexfrabdioph  41220  7rexfrabdioph  41221  eldioph4i  41233  diophren  41234  pell1qrval  41267  pell14qrval  41269  pell1234qrval  41271  rpnnen3  41454  fnwe2lem1  41475  pwssplit4  41514  pwslnmlem2  41518  dgraaval  41569  itgoval  41586  rgspnval  41593  proot1hash  41625  rp-intrabeq  41653  rp-unirabeq  41654  rfovfvd  42436  rfovfvfvd  42437  rfovcnvf1od  42438  fsovrfovd  42443  fsovfvd  42444  fsovfvfvd  42445  fsovcnvlem  42447  nzss  42759  supminfxr  43859  dvnprodlem1  44347  dvnprodlem2  44348  dvnprodlem3  44349  dvnprod  44350  stoweidlem26  44427  stoweidlem27  44428  stoweidlem31  44432  stoweidlem34  44435  stoweidlem46  44447  fourierdlem79  44586  fourierdlem96  44603  fourierdlem97  44604  fourierdlem98  44605  fourierdlem99  44606  fourierdlem105  44612  fourierdlem107  44614  fourierdlem108  44615  fourierdlem110  44617  etransclem11  44646  salgenval  44722  subsaliuncl  44759  ovnval  44942  ovnval2  44946  ovnval2b  44953  ovncvrrp  44965  ovnsubaddlem1  44971  ovnsubadd  44973  ovncvr2  45012  hspmbl  45030  ovolval2  45045  ovnovollem3  45059  salpreimagelt  45108  salpreimalegt  45110  salpreimagtge  45126  salpreimaltle  45127  issmflem  45128  issmf  45129  salpreimagtlt  45131  smfpreimalt  45132  smfpreimaltf  45137  issmfle  45146  smfpimltxr  45148  smfpreimale  45155  issmfgt  45157  smfpreimagt  45163  issmfge  45171  smflimlem3  45174  smflimlem4  45175  smflim  45178  smfpimgtxr  45181  smfpreimage  45183  fvmptrabdm  45685  elsetpreimafveq  45749  prmdvdsfmtnof1  45939  fppr  46078  rnghmval  46349  bigoval  46795  line  46978  rrxline  46980  sphere  46993  line2y  47001  inpw  47063