Theorem opabbidv 4917

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  {copab 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-opab 4914

This theorem is referenced by:  opabbii  4918  csbopab  5210  csbopabgALT  5211  csbmpt12  5212  xpeq1  5332  xpeq2  5338  opabbi2dv  5480  csbcnvgALT  5515  resopab2  5660  mptcnv  5752  cores  5859  xpco  5896  dffn5  6465  f1oiso2  6829  fvmptopab  6930  f1ocnvd  7117  ofreq  7133  mptmpt2opabbrd  7484  bropopvvv  7492  bropfvvvv  7494  fnwelem  7529  sprmpt2d  7588  mpt2curryd  7633  wemapwe  8844  xpcogend  13941  shftfval  14036  2shfti  14046  prdsval  16323  pwsle  16360  sectffval  16617  sectfval  16618  isfunc  16731  isfull  16777  isfth  16781  ipoval  17362  eqgfval  17847  dvdsrval  18850  dvdsrpropd  18901  ltbval  19683  opsrval  19686  lmfval  21254  xkocnv  21835  tgphaus  22137  isphtpc  23010  bcthlem1  23338  bcth  23343  ulmval  24354  lgsquadlem3  25327  iscgrg  25627  legval  25699  ishlg  25717  perpln1  25825  perpln2  25826  isperp  25827  ishpg  25871  iscgra  25921  isinag  25949  isleag  25953  wksfval  26739  upgrtrls  26832  upgrspthswlk  26868  ajfval  27998  f1o3d  29764  f1od2  29832  inftmrel  30065  isinftm  30066  metidval  30264  faeval  30640  eulerpartlemgvv  30769  eulerpart  30775  afsval  31080  cureq  33700  curf  33702  curunc  33706  fnopabeqd  33828  cosseq  34496  lcvfbr  34802  cmtfvalN  34992  cvrfval  35050  dicffval  36956  dicfval  36957  dicval  36958  dnwech  38120  aomclem8  38133  rfovcnvfvd  38802  fsovrfovd  38804  dfafn5a  41750  upwlksfval  42285  sprsymrelfv  42313  sprsymrelfo  42316