Theorem opabbidv 5028

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  {copab 5024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-opab 5025

This theorem is referenced by:  opabbii  5029  csbopab  5330  csbopabgALT  5331  csbmpt12  5332  xpeq1  5457  xpeq2  5464  opabbi2dv  5606  csbcnvgALT  5641  resopab2  5785  mptcnv  5874  cores  5977  xpco  6015  dffn5  6592  f1oiso2  6968  fvmptopab  7068  f1ocnvd  7254  ofreq  7270  mptmpoopabbrd  7634  bropopvvv  7641  bropfvvvv  7643  fnwelem  7678  sprmpod  7741  mpocurryd  7786  wemapwe  9006  xpcogend  14168  shftfval  14263  2shfti  14273  prdsval  16557  pwsle  16594  sectffval  16849  sectfval  16850  isfunc  16963  isfull  17009  isfth  17013  ipoval  17593  eqgfval  18081  dvdsrval  19085  dvdsrpropd  19136  ltbval  19939  opsrval  19942  lmfval  21524  xkocnv  22106  tgphaus  22408  isphtpc  23281  bcthlem1  23610  bcth  23615  ulmval  24651  lgsquadlem3  25640  iscgrg  25980  legval  26052  ishlg  26070  perpln1  26178  perpln2  26179  isperp  26180  ishpg  26227  iscgra  26277  isinag  26307  isleag  26316  wksfval  27074  upgrtrls  27170  upgrspthswlk  27206  ajfval  28277  f1o3d  30062  f1od2  30145  inftmrel  30447  isinftm  30448  metidval  30747  faeval  31122  eulerpartlemgvv  31251  eulerpart  31257  afsval  31559  satf  32209  satfvsuc  32217  satfv1  32219  satf0suc  32232  sat1el2xp  32235  fmlasuc0  32240  cureq  34418  curf  34420  curunc  34424  fnopabeqd  34546  cosseq  35221  lcvfbr  35706  cmtfvalN  35896  cvrfval  35954  dicffval  37860  dicfval  37861  dicval  37862  prjspval  38769  prjspnval2  38783  0prjspn  38786  dnwech  39152  aomclem8  39165  rfovcnvfvd  39857  fsovrfovd  39859  dfafn5a  42895  sprsymrelfv  43158  sprsymrelfo  43161  upwlksfval  43512