MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abbidv Structured version   Visualization version   GIF version

Theorem abbidv 2738
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
abbidv (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1840 . 2 𝑥𝜑
2 abbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2abbid 2737 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  {cab 2607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617
This theorem is referenced by:  rabbidva2  3177  cdeqab  3411  sbceqbid  3428  csbeq1  3521  csbeq2  3522  csbprc  3957  csbprcOLD  3958  sbcel12  3960  sbceqg  3961  csbeq2d  3968  csbnestgf  3973  pweq  4138  sneq  4163  csbsng  4219  rabsn  4231  unieq  4415  csbuni  4437  inteq  4448  iineq1  4506  iineq2  4509  dfiin2g  4524  iinrab  4553  iinxprg  4572  opabbid  4682  imasng  5451  iotaeq  5823  iotabi  5824  dfimafn  6207  fnsnfv  6220  fliftf  6525  oprabbid  6668  wrecseq123  7360  rdglim2  7480  qseq1  7748  qseq2  7749  qsinxp  7775  mapvalg  7819  ixpsnval  7862  ixpeq1  7870  fival  8269  tcvalg  8565  karden  8709  acneq  8817  infmap2  8991  cfval  9020  cflim3  9035  axdclem  9292  axdc  9294  rankcf  9550  genpv  9772  negfi  10922  supadd  10942  hashf1lem2  13185  hashf1  13186  hashfac  13187  csbwrdg  13280  cshimadifsn  13519  cshimadifsn0  13520  cleq1  13663  dfrtrcl2  13743  shftlem  13749  shftfib  13753  vdwlem6  15621  cshwsiun  15737  lubfval  16906  glbfval  16919  eqglact  17573  isghm  17588  symgval  17727  sylow1lem2  17942  sylow3lem1  17970  efgval  18058  dmdprd  18325  ixpsnbasval  19137  aspval2  19275  ressmplbas2  19383  cssval  19954  tgval  20679  clsval2  20773  lpfval  20861  lpval  20862  islocfin  21239  ptval  21292  hauspwpwf1  21710  ptcmplem2  21776  snclseqg  21838  ustval  21925  itg2val  23414  limcfval  23555  plyval  23866  isismt  25342  nb3grprlem1  26182  vtxdun  26276  rgrx0ndm  26372  ewlksfval  26380  wwlksnfi  26683  rusgrnumwwlkb0  26746  eclclwwlksn1  26831  avril1  27186  nmoofval  27484  nmooval  27485  nmoo0  27513  nmopval  28582  nmfnval  28602  iunrdx  29245  disjabrex  29258  disjabrexf  29259  dfimafnf  29297  curry2ima  29347  pstmval  29738  pstmfval  29739  sigaval  29972  measval  30060  orvcval  30318  bnj956  30582  bnj18eq1  30732  bnj1318  30828  derangval  30884  mclsval  31195  dfrdg2  31429  dfrdg3  31430  altxpeq1  31749  altxpeq2  31750  bj-snsetex  32625  bj-sngleq  32629  bj-projeq  32654  bj-projval  32658  csbwrecsg  32832  csboprabg  32835  finxpeq1  32882  finxpeq2  32883  csbfinxpg  32884  finxpreclem6  32892  ptrest  33067  poimirlem26  33094  poimirlem27  33095  poimirlem28  33096  mblfinlem3  33107  cnambfre  33117  itg2addnc  33123  areacirclem5  33163  sdclem2  33197  sdc  33199  ismtyval  33258  elghomlem1OLD  33343  iineq12f  33632  lfl1dim  33915  ldual1dim  33960  glbconxN  34171  lineset  34531  pointsetN  34534  psubspset  34537  pmapglb2xN  34565  polval2N  34699  psubclsetN  34729  lautset  34875  pautsetN  34891  tendofset  35553  tendoset  35554  dva1dim  35780  dia1dim2  35858  dib1dim2  35964  diclspsn  35990  dih1dimatlem  36125  dihglb2  36138  hdmap1ffval  36592  hdmapffval  36625  hgmapffval  36684  eldiophb  36827  eldioph  36828  diophrw  36829  eldioph2  36832  eldioph2b  36833  eldioph3  36836  diophin  36843  diophun  36844  diophrex  36846  rexrabdioph  36865  rmxypairf1o  36983  hbtlem1  37201  hbtlem7  37203  nzss  38025  dropab1  38160  dropab2  38161  sbcel12gOLD  38263  csbunigOLD  38561  csbfv12gALTOLD  38562  csbxpgOLD  38563  csbrngOLD  38566  supsubc  39056  dfaimafn  40570  rnfdmpr  40618  fargshiftfo  40697  sprval  41038  sprvalpw  41039  setrecseq  41746
  Copyright terms: Public domain W3C validator