Theorem rabbidv 3386

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ∈ wcel 2157  {crab 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-ral 3108  df-rab 3112

This theorem is referenced by:  rabeqbidv  3392  difeq2  3928  seex  5281  mptiniseg  5850  dfpred3g  5911  elovmpt2rab  7113  elovmpt3rab1  7126  fineqvlem  8416  mapfien2  8556  supeq1  8593  supeq2  8596  supeq3  8597  oieq1  8659  oieq2  8660  ordtypecbv  8664  ordtypelem3  8667  harval  8709  inf3lema  8771  wemapwe  8844  oef1o  8845  tz9.12lem3  8902  rankvalb  8910  rankvalg  8930  ranksnb  8940  rankonidlem  8941  cardval3  9064  cardidm  9071  alephsuc2  9189  coftr  9383  fin1a2lem11  9520  fin1a2lem12  9521  hsmex  9542  axdc3lem2  9561  zorn2lem1  9606  zorn2lem6  9611  zorn2lem7  9612  zorn2g  9613  wuncval  9852  tskmval  9949  peano5uzti  11736  uzval  11909  rpnnen1  12042  ixxval  12404  fzval  12554  hashbclem  13456  hashbc  13457  shftfn  14039  bitsfval  15367  sadfval  15396  sadcom  15407  smufval  15421  smupp1  15424  smupval  15432  smumullem  15436  gcdval  15440  bezoutlem2  15479  bezoutlem4  15481  lcmval  15527  lcmfval  15556  lcmf0val  15557  lcmfpr  15562  isprm  15608  odzval  15716  pcval  15769  pceulem  15770  pceu  15771  pczpre  15772  pcdiv  15777  prmreclem1  15840  prmreclem4  15843  prmreclem5  15844  ramval  15932  cshws0  16023  imasdsval  16383  mrcval  16478  eldmcoa  16922  cycsubg2  17836  cntzval  17958  cntzsnval  17961  odfval  18156  odval  18157  gexval  18197  efgsfo  18356  dprdval  18607  ablfac1a  18673  ablfac1b  18674  ablfac1eu  18677  ablfaclem1  18689  ablfaclem3  18691  lspval  19185  aspval  19540  psrass1lem  19589  psrmulval  19598  mplmonmul  19676  coe1mul2  19850  ocvval  20225  dsmmelbas  20297  frlmsslss  20327  pmatcoe1fsupp  20723  istopon  20934  toponsspwpw  20944  clsval  21059  neival  21124  ordtbaslem  21210  ordtbas2  21213  ordtopn1  21216  ordtopn2  21217  cnpval  21258  llyeq  21491  nllyeq  21492  ptfinfin  21540  finlocfin  21541  dissnlocfin  21550  locfindis  21551  xkoopn  21610  kqfval  21744  tsmsfbas  22148  blvalps  22407  blval  22408  nmofval  22735  nmoval  22736  ishtpy  22988  minveclem3b  23417  minveclem3  23418  minveclem4  23421  minveclem5  23422  ovolval  23460  vitalilem2  23596  vitalilem3  23597  vitalilem4  23598  vitali  23600  itg2monolem1  23737  elcpn  23917  mdegmullem  24058  elqaalem1  24294  elqaalem2  24295  elqaalem3  24296  elqaa  24297  aannenlem1  24303  aannenlem2  24304  jensen  24935  vmaval  25059  muval  25078  sgmval  25088  fsumdvdscom  25131  musum  25137  muinv  25139  dchrisum0fval  25414  dchrisum0ff  25416  logsqvma2  25452  pntrlog2bndlem1  25486  tglngval  25666  ttgval  25975  ttgitvval  25982  ebtwntg  26082  numedglnl  26260  dfnbgr2  26452  dfnbgr3  26453  uvtxusgr  26531  vtxdgval  26598  rusgrnumwrdl2  26716  iswwlksnon  26981  iswwlksnonOLD  26982  rusgrnumwwlks  27122  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  clwwlknon  27261  clwwlknonOLD  27262  clwwlk0on0  27265  clwwlknondisjOLD  27291  eupth2  27418  fusgreg2wsplem  27514  fusgreghash2wsp  27519  numclwlk1lem1  27555  numclwwlk3lemOLD  27575  sspval  27912  ubthlem1  28060  ubthlem2  28061  ubthlem3  28062  ocval  28473  spanval  28526  chsupid  28605  eigvecval  29089  specval  29091  iunpreima  29714  crefeq  30243  ordtcnvNEW  30297  ordtrest2NEW  30300  ordtconnlem1  30301  measvuni  30608  brfae  30642  omsfval  30687  orvcelval  30861  ballotlemi  30893  bnj602  31313  subfacp1lem6  31495  kur14  31526  cvmscbv  31568  cvmsi  31575  cvmsval  31576  snmlval  31641  snmlflim  31642  scutval  32237  fvray  32574  fwddifnval  32596  neibastop3  32683  icoreval  33519  fin2so  33711  poimirlem26  33750  poimirlem27  33751  poimirlem28  33752  poimirlem32  33756  ftc1anclem6  33804  islinei  35522  pmapval  35539  paddval  35580  paddcom  35595  pclvalN  35672  ldilset  35891  dilsetN  35935  diafval  36813  diaval  36814  docavalN  36905  dicfval  36957  dochfval  37132  dochval  37133  mapdval  37410  mapdsn2  37424  2rexfrabdioph  37863  3rexfrabdioph  37864  4rexfrabdioph  37865  6rexfrabdioph  37866  7rexfrabdioph  37867  eldioph4i  37879  diophren  37880  pell1qrval  37913  pell14qrval  37915  pell1234qrval  37917  rpnnen3  38101  fnwe2lem1  38122  pwssplit4  38161  pwslnmlem2  38165  dgraaval  38216  itgoval  38233  rgspnval  38240  proot1hash  38280  rfovfvd  38797  rfovfvfvd  38798  rfovcnvf1od  38799  fsovrfovd  38804  fsovfvd  38805  fsovfvfvd  38806  fsovcnvlem  38808  nzss  39017  supminfxr  40174  dvnprodlem1  40642  dvnprodlem2  40643  dvnprodlem3  40644  dvnprod  40645  stoweidlem26  40723  stoweidlem27  40724  stoweidlem31  40728  stoweidlem34  40731  stoweidlem46  40743  fourierdlem79  40882  fourierdlem96  40899  fourierdlem97  40900  fourierdlem98  40901  fourierdlem99  40902  fourierdlem105  40908  fourierdlem107  40910  fourierdlem108  40911  fourierdlem110  40913  etransclem11  40942  salgenval  41021  subsaliuncl  41056  ovnval  41238  ovnval2  41242  ovnval2b  41249  ovncvrrp  41261  ovnsubaddlem1  41267  ovnsubadd  41269  ovncvr2  41308  hspmbl  41326  ovolval2  41341  ovnovollem3  41355  salpreimagelt  41401  salpreimalegt  41403  salpreimagtge  41417  salpreimaltle  41418  issmflem  41419  issmf  41420  salpreimagtlt  41422  smfpreimalt  41423  smfpreimaltf  41428  issmfle  41437  smfpimltxr  41439  smfpreimale  41446  issmfgt  41448  smfpreimagt  41453  issmfge  41461  smflimlem3  41464  smflimlem4  41465  smflim  41468  smfpimgtxr  41471  smfpreimage  41473  fvmptrabdm  41884  prmdvdsfmtnof1  42075  rnghmval  42460  bigoval  42912