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

Theorem opabbidv 5099
 Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
opabbidv (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem opabbidv
StepHypRef Expression
1 nfv 1915 . 2 𝑥𝜑
2 nfv 1915 . 2 𝑦𝜑
3 opabbidv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3opabbid 5098 1 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  {copab 5095 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 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-opab 5096 This theorem is referenced by:  opabbii  5100  csbopab  5410  csbopabgALT  5411  csbmpt12  5412  xpeq1  5537  xpeq2  5544  opabbi2dv  5688  csbcnvgALT  5723  resopab2  5875  mptcnv  5969  cores  6073  xpco  6112  dffn5  6703  f1oiso2  7088  fvmptopab  7192  f1ocnvd  7380  ofreq  7396  mptmpoopabbrd  7765  bropopvvv  7772  bropfvvvv  7774  fnwelem  7812  sprmpod  7877  mpocurryd  7922  wemapwe  9148  xpcogend  14329  shftfval  14424  2shfti  14434  prdsval  16723  pwsle  16760  sectffval  17015  sectfval  17016  isfunc  17129  isfull  17175  isfth  17179  ipoval  17759  eqgfval  18323  dvdsrval  19394  dvdsrpropd  19445  ltbval  20714  opsrval  20717  lmfval  21840  xkocnv  22422  tgphaus  22725  isphtpc  23602  bcthlem1  23931  bcth  23936  ulmval  24978  lgsquadlem3  25969  iscgrg  26309  legval  26381  ishlg  26399  perpln1  26507  perpln2  26508  isperp  26509  ishpg  26556  iscgra  26606  isinag  26635  isleag  26644  wksfval  27402  upgrtrls  27494  upgrspthswlk  27530  ajfval  28595  f1o3d  30389  f1od2  30486  mgcoval  30697  inftmrel  30862  isinftm  30863  idlsrgval  31056  metidval  31241  faeval  31613  eulerpartlemgvv  31742  eulerpart  31748  afsval  32050  satf  32708  satfvsuc  32716  satfv1  32718  satf0suc  32731  sat1el2xp  32734  fmlasuc0  32739  bj-imdirvallem  34590  bj-imdirval2  34593  bj-imdirco  34600  bj-iminvval2  34604  cureq  35026  curf  35028  curunc  35032  fnopabeqd  35151  cosseq  35824  lcvfbr  36309  cmtfvalN  36499  cvrfval  36557  dicffval  38463  dicfval  38464  dicval  38465  prjspval  39584  prjspnval2  39598  0prjspn  39601  dnwech  39979  aomclem8  39992  rfovcnvfvd  40695  fsovrfovd  40697  dfafn5a  43703  sprsymrelfv  43998  sprsymrelfo  44001  upwlksfval  44350
 Copyright terms: Public domain W3C validator