Theorem opabbidv 5123

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

Step	Hyp	Ref	Expression
1		nfv 1909	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1909	. 2 ⊢ Ⅎ𝑦𝜑
3		opabbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 2, 3	opabbid 5122	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1531  {copab 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-opab 5120

This theorem is referenced by:  opabbii  5124  csbopab  5433  csbopabgALT  5434  csbmpt12  5435  xpeq1  5562  xpeq2  5569  opabbi2dv  5713  csbcnvgALT  5748  resopab2  5897  mptcnv  5991  cores  6095  xpco  6133  dffn5  6717  f1oiso2  7097  fvmptopab  7201  f1ocnvd  7388  ofreq  7404  mptmpoopabbrd  7770  bropopvvv  7777  bropfvvvv  7779  fnwelem  7817  sprmpod  7882  mpocurryd  7927  wemapwe  9152  xpcogend  14326  shftfval  14421  2shfti  14431  prdsval  16720  pwsle  16757  sectffval  17012  sectfval  17013  isfunc  17126  isfull  17172  isfth  17176  ipoval  17756  eqgfval  18320  dvdsrval  19387  dvdsrpropd  19438  ltbval  20244  opsrval  20247  lmfval  21832  xkocnv  22414  tgphaus  22717  isphtpc  23590  bcthlem1  23919  bcth  23924  ulmval  24960  lgsquadlem3  25950  iscgrg  26290  legval  26362  ishlg  26380  perpln1  26488  perpln2  26489  isperp  26490  ishpg  26537  iscgra  26587  isinag  26616  isleag  26625  wksfval  27383  upgrtrls  27475  upgrspthswlk  27511  ajfval  28578  f1o3d  30364  f1od2  30449  inftmrel  30802  isinftm  30803  metidval  31123  faeval  31498  eulerpartlemgvv  31627  eulerpart  31633  afsval  31935  satf  32593  satfvsuc  32601  satfv1  32603  satf0suc  32616  sat1el2xp  32619  fmlasuc0  32624  bj-imdirval  34464  bj-imdirval2  34465  bj-imdirid  34467  cureq  34860  curf  34862  curunc  34866  fnopabeqd  34987  cosseq  35663  lcvfbr  36148  cmtfvalN  36338  cvrfval  36396  dicffval  38302  dicfval  38303  dicval  38304  prjspval  39244  prjspnval2  39258  0prjspn  39261  dnwech  39639  aomclem8  39652  rfovcnvfvd  40344  fsovrfovd  40346  dfafn5a  43350  sprsymrelfv  43647  sprsymrelfo  43650  upwlksfval  44001