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

Theorem opabbii 4684
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbii.1 (𝜑𝜓)
Assertion
Ref Expression
opabbii {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Proof of Theorem opabbii
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eqid 2621 . 2 𝑧 = 𝑧
2 opabbii.1 . . . 4 (𝜑𝜓)
32a1i 11 . . 3 (𝑧 = 𝑧 → (𝜑𝜓))
43opabbidv 4683 . 2 (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
51, 4ax-mp 5 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1480  {copab 4677
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  df-opab 4679
This theorem is referenced by:  mptv  4716  2rbropap  4982  dfid4  4996  fconstmpt  5128  xpundi  5137  xpundir  5138  inxp  5219  csbcnv  5271  cnvco  5273  resopab  5410  opabresid  5419  cnvi  5501  cnvun  5502  cnvxp  5515  cnvcnv3  5546  coundi  5600  coundir  5601  mptun  5987  fvopab6  6271  fmptsng  6394  fmptsnd  6395  cbvoprab1  6687  cbvoprab12  6689  dmoprabss  6702  mpt2mptx  6711  resoprab  6716  elrnmpt2res  6734  ov6g  6758  1st2val  7146  2nd2val  7147  dfoprab3s  7175  dfoprab3  7176  dfoprab4  7177  opabn1stprc  7180  mptmpt2opabbrd  7200  fsplit  7234  mapsncnv  7856  xpcomco  8002  marypha2lem2  8294  oemapso  8531  leweon  8786  r0weon  8787  compsscnv  9145  fpwwe  9420  ltrelxr  10051  ltxrlt  10060  ltxr  11901  shftidt2  13763  prdsle  16054  prdsless  16055  prdsleval  16069  dfiso2  16364  joindm  16935  meetdm  16949  gaorb  17672  efgcpbllema  18099  frgpuplem  18117  ltbval  19403  ltbwe  19404  opsrle  19407  opsrtoslem1  19416  opsrtoslem2  19417  dvdsrzring  19763  pjfval2  19985  lmfval  20959  lmbr  20985  cnmptid  21387  lgsquadlem3  25024  perpln1  25522  outpasch  25564  ishpg  25568  axcontlem2  25762  wksfval  26392  wlkson  26438  pthsfval  26503  ispth  26505  dfadj2  28614  dmadjss  28616  cnvadj  28621  mpt2mptxf  29343  fneer  32025  bj-dfmpt2a  32743  bj-mpt2mptALT  32744  opropabco  33185  cmtfvalN  34012  cmtvalN  34013  cvrfval  34070  cvrval  34071  dicval2  35983  fgraphopab  37304  fgraphxp  37305  opabbrfex0d  40628  opabbrfexd  40630  upwlksfval  41030  xpsnopab  41079  mpt2mptx2  41427
  Copyright terms: Public domain W3C validator