Theorem opabbidv 4749

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 1883	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1883	. 2 ⊢ Ⅎ𝑦𝜑
3		opabbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 2, 3	opabbid 4748	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  {copab 4745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746

This theorem is referenced by:  opabbii  4750  csbopab  5037  csbopabgALT  5038  csbmpt12  5039  xpeq1  5157  xpeq2  5163  opabbi2dv  5304  csbcnvgALT  5339  resopab2  5483  mptcnv  5569  cores  5676  xpco  5713  dffn5  6280  f1oiso2  6642  fvmptopab  6739  f1ocnvd  6926  ofreq  6942  mptmpt2opabbrd  7293  bropopvvv  7300  bropfvvvv  7302  fnwelem  7337  sprmpt2d  7395  mpt2curryd  7440  wemapwe  8632  xpcogend  13759  shftfval  13854  2shfti  13864  prdsval  16162  pwsle  16199  sectffval  16457  sectfval  16458  isfunc  16571  isfull  16617  isfth  16621  ipoval  17201  eqgfval  17689  dvdsrval  18691  dvdsrpropd  18742  ltbval  19519  opsrval  19522  lmfval  21084  xkocnv  21665  tgphaus  21967  isphtpc  22840  bcthlem1  23167  bcth  23172  ulmval  24179  lgsquadlem3  25152  iscgrg  25452  legval  25524  ishlg  25542  perpln1  25650  perpln2  25651  isperp  25652  ishpg  25696  iscgra  25746  isinag  25774  isleag  25778  wksfval  26561  upgrtrls  26654  upgrspthswlk  26690  ajfval  27792  f1o3d  29559  f1od2  29627  inftmrel  29862  isinftm  29863  metidval  30061  faeval  30437  eulerpartlemgvv  30566  eulerpart  30572  afsval  30877  cureq  33515  curf  33517  curunc  33521  fnopabeqd  33644  cosseq  34321  lcvfbr  34625  cmtfvalN  34815  cvrfval  34873  dicffval  36780  dicfval  36781  dicval  36782  dnwech  37935  aomclem8  37948  rfovcnvfvd  38618  fsovrfovd  38620  dfafn5a  41561  upwlksfval  42041  sprsymrelfv  42069  sprsymrelfo  42072