Theorem rabbidv 3403

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-rab 3397

This theorem is referenced by:  difeq2  4069  seex  5578  mptiniseg  6191  dfpred3g  6265  elovmporab  7598  elovmpt3rab1  7612  naddcllem  8597  naddov2  8600  naddcom  8603  naddrid  8604  naddass  8617  fineqvlem  9157  mapfien2  9300  supeq1  9336  supeq2  9339  supeq3  9340  oieq1  9405  oieq2  9406  ordtypecbv  9410  ordtypelem3  9413  harval  9453  inf3lema  9521  wemapwe  9594  oef1o  9595  tz9.12lem3  9689  rankvalb  9697  rankvalg  9717  ranksnb  9727  rankonidlem  9728  cardval3  9852  cardidm  9859  alephsuc2  9978  coftr  10171  fin1a2lem11  10308  fin1a2lem12  10309  hsmex  10330  axdc3lem2  10349  zorn2lem1  10394  zorn2lem6  10399  zorn2lem7  10400  zorn2g  10401  wuncval  10640  tskmval  10737  peano5uzti  12569  uzval  12740  rpnnen1  12883  ixxval  13255  fzval  13411  hashbclem  14361  hashbc  14362  shftfn  14982  bitsfval  16336  sadfval  16365  sadcom  16376  smufval  16390  smupp1  16393  smupval  16401  smumullem  16405  gcdval  16409  bezoutlem2  16453  bezoutlem4  16455  lcmval  16505  lcmfval  16534  lcmf0val  16535  lcmfpr  16540  isprm  16586  odzval  16705  pcval  16758  pceulem  16759  pceu  16760  pczpre  16761  pcdiv  16766  prmreclem1  16830  prmreclem4  16833  prmreclem5  16834  ramval  16922  cshws0  17015  imasdsval  17421  mrcval  17518  eldmcoa  17974  chneq1  18520  cycsubg2  19124  cntzval  19235  cntzsnval  19238  odfval  19446  odfvalALT  19447  odval  19448  gexval  19492  efgsfo  19653  dprdval  19919  ablfac1a  19985  ablfac1b  19986  ablfac1eu  19989  ablfaclem1  20001  ablfaclem3  20003  rnghmval  20360  rgspnval  20529  lspval  20910  ocvval  21606  dsmmelbas  21678  frlmsslss  21713  aspval  21812  psrass1lem  21871  psrmulval  21883  mplmonmul  21972  mhpval  22055  mhpmulcl  22065  coe1mul2  22184  pmatcoe1fsupp  22617  istopon  22828  toponsspwpw  22838  clsval  22953  neival  23018  ordtbaslem  23104  ordtbas2  23107  ordtopn1  23110  ordtopn2  23111  cnpval  23152  llyeq  23386  nllyeq  23387  ptfinfin  23435  finlocfin  23436  dissnlocfin  23445  locfindis  23446  xkoopn  23505  kqfval  23639  tsmsfbas  24044  blvalps  24301  blval  24302  nmofval  24630  nmoval  24631  ishtpy  24899  minveclem3b  25356  minveclem3  25357  minveclem4  25360  minveclem5  25361  ovolval  25402  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  vitali  25542  itg2monolem1  25679  elcpn  25864  mdegmullem  26011  elqaalem1  26255  elqaalem2  26256  elqaalem3  26257  elqaa  26258  aannenlem1  26264  aannenlem2  26265  jensen  26927  vmaval  27051  muval  27070  sgmval  27080  fsumdvdscom  27123  musum  27129  muinv  27131  dchrisum0fval  27444  dchrisum0ff  27446  logsqvma2  27482  pntrlog2bndlem1  27516  scutval  27742  bdayon  28210  tglngval  28530  ttgval  28854  ttgitvval  28861  ebtwntg  28962  numedglnl  29124  dfnbgr2  29317  dfnbgr3  29318  uvtxusgr  29382  vtxdgval  29449  rusgrnumwrdl2  29567  iswwlksnon  29833  rusgrnumwwlks  29957  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  clwlknf1oclwwlknlem2  30064  clwwlknon  30072  clwwlk0on0  30074  eupth2  30221  fusgreg2wsplem  30315  fusgreghash2wsp  30320  numclwlk1lem1  30351  sspval  30705  ubthlem1  30852  ubthlem2  30853  ubthlem3  30854  ocval  31262  spanval  31315  chsupid  31394  eigvecval  31878  specval  31880  iunpreima  32546  fcobijfs2  32709  pwrssmgc  32988  fxpgaval  33143  nsgqusf1olem3  33387  mplvrpmrhm  33595  esplyfval  33604  minplyval  33739  constrsuc  33772  constrcbvlem  33789  crefeq  33879  zarcls1  33903  zarclsun  33904  zarclsiin  33905  zarclsint  33906  zarclssn  33907  zartop  33910  zartopon  33911  zart0  33913  zarmxt1  33914  zarcmp  33916  rhmpreimacnlem  33918  rhmpreimacn  33919  ordtcnvNEW  33954  ordtrest2NEW  33957  ordtconnlem1  33958  measvuni  34248  brfae  34282  omsfval  34328  orvcelval  34503  ballotlemi  34535  bnj602  34948  fineqvnttrclselem2  35163  fineqvnttrclselem3  35164  fineqvnttrclse  35165  onvf1odlem3  35170  subfacp1lem6  35250  kur14  35281  cvmscbv  35323  cvmsi  35330  cvmsval  35331  snmlval  35396  snmlflim  35397  satfv0  35423  satfv1  35428  satfv0fun  35436  satffunlem1lem1  35467  satffunlem2lem1  35469  satfv0fvfmla0  35478  satfv1fvfmla1  35488  prv1n  35496  fvray  36206  fwddifnval  36228  neibastop3  36427  weiunlem2  36528  icoreval  37418  fin2so  37667  poimirlem26  37706  poimirlem27  37707  poimirlem28  37708  poimirlem32  37712  ftc1anclem6  37758  islinei  39859  pmapval  39876  paddval  39917  paddcom  39932  pclvalN  40009  ldilset  40228  dilsetN  40272  diafval  41150  diaval  41151  docavalN  41242  dicfval  41294  dochfval  41469  dochval  41470  mapdval  41747  mapdsn2  41761  grpods  42307  unitscyglem1  42308  unitscyglem2  42309  unitscyglem3  42310  unitscyglem4  42311  prjcrvval  42750  2rexfrabdioph  42913  3rexfrabdioph  42914  4rexfrabdioph  42915  6rexfrabdioph  42916  7rexfrabdioph  42917  eldioph4i  42929  diophren  42930  pell1qrval  42963  pell14qrval  42965  pell1234qrval  42967  rpnnen3  43149  fnwe2lem1  43167  pwssplit4  43206  pwslnmlem2  43210  dgraaval  43261  itgoval  43278  proot1hash  43312  rp-intrabeq  43338  rp-unirabeq  43339  rfovfvd  44119  rfovfvfvd  44120  rfovcnvf1od  44121  fsovrfovd  44126  fsovfvd  44127  fsovfvfvd  44128  fsovcnvlem  44130  nzss  44434  supminfxr  45586  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  dvnprod  46071  stoweidlem26  46148  stoweidlem27  46149  stoweidlem31  46153  stoweidlem34  46156  stoweidlem46  46168  fourierdlem79  46307  fourierdlem96  46324  fourierdlem97  46325  fourierdlem98  46326  fourierdlem99  46327  fourierdlem105  46333  fourierdlem107  46335  fourierdlem108  46336  fourierdlem110  46338  etransclem11  46367  salgenval  46443  subsaliuncl  46480  ovnval  46663  ovnval2  46667  ovnval2b  46674  ovncvrrp  46686  ovnsubaddlem1  46692  ovnsubadd  46694  ovncvr2  46733  hspmbl  46751  ovolval2  46766  ovnovollem3  46780  salpreimagelt  46829  salpreimalegt  46831  salpreimagtge  46847  salpreimaltle  46848  issmflem  46849  issmf  46850  salpreimagtlt  46852  smfpreimalt  46853  smfpreimaltf  46858  issmfle  46867  smfpimltxr  46869  smfpreimale  46876  issmfgt  46878  smfpreimagt  46884  issmfge  46892  smflimlem3  46895  smflimlem4  46896  smflim  46899  smfpimgtxr  46902  smfpreimage  46904  fvmptrabdm  47417  elsetpreimafveq  47521  prmdvdsfmtnof1  47711  fppr  47850  dfclnbgr2  47947  dfclnbgr3  47950  dfsclnbgr6  47982  grlimedgclnbgr  48119  grlimgrtri  48127  grilcbri2  48135  bigoval  48674  line  48857  rrxline  48859  sphere  48872  line2y  48880  inpw  48949