Theorem opabbidv 4716

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (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 1843	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1843	. 2 ⊢ Ⅎ𝑦𝜑
3		opabbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 2, 3	opabbid 4715	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  {copab 4712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713

This theorem is referenced by:  opabbii  4717  csbopab  5008  csbopabgALT  5009  csbmpt12  5010  xpeq1  5128  xpeq2  5129  opabbi2dv  5271  csbcnvgALT  5307  resopab2  5448  mptcnv  5534  cores  5638  xpco  5675  dffn5  6241  f1oiso2  6602  fvmptopab  6697  f1ocnvd  6884  ofreq  6900  mptmpt2opabbrd  7248  bropopvvv  7255  bropfvvvv  7257  fnwelem  7292  sprmpt2d  7350  mpt2curryd  7395  wemapwe  8594  xpcogend  13713  shftfval  13810  2shfti  13820  prdsval  16115  pwsle  16152  sectffval  16410  sectfval  16411  isfunc  16524  isfull  16570  isfth  16574  ipoval  17154  eqgfval  17642  dvdsrval  18645  dvdsrpropd  18696  ltbval  19471  opsrval  19474  lmfval  21036  xkocnv  21617  tgphaus  21920  isphtpc  22793  bcthlem1  23121  bcth  23126  ulmval  24134  lgsquadlem3  25107  iscgrg  25407  legval  25479  ishlg  25497  perpln1  25605  perpln2  25606  isperp  25607  ishpg  25651  iscgra  25701  isinag  25729  isleag  25733  wksfval  26505  upgrtrls  26598  upgrspthswlk  26634  ajfval  27664  f1o3d  29431  f1od2  29499  inftmrel  29734  isinftm  29735  metidval  29933  faeval  30309  eulerpartlemgvv  30438  eulerpart  30444  afsval  30749  cureq  33385  curf  33387  curunc  33391  fnopabeqd  33514  lcvfbr  34307  cmtfvalN  34497  cvrfval  34555  dicffval  36463  dicfval  36464  dicval  36465  dnwech  37618  aomclem8  37631  rfovcnvfvd  38301  fsovrfovd  38303  dfafn5a  41240  upwlksfval  41716  sprsymrelfv  41744  sprsymrelfo  41747