Theorem opabbidv 5132

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  {copab 5128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-opab 5129

This theorem is referenced by:  opabbii  5133  csbopab  5442  csbopabgALT  5443  csbmpt12  5444  xpeq1  5569  xpeq2  5576  opabbi2dv  5720  csbcnvgALT  5755  resopab2  5904  mptcnv  5998  cores  6102  xpco  6140  dffn5  6724  f1oiso2  7105  fvmptopab  7209  f1ocnvd  7396  ofreq  7412  mptmpoopabbrd  7778  bropopvvv  7785  bropfvvvv  7787  fnwelem  7825  sprmpod  7890  mpocurryd  7935  wemapwe  9160  xpcogend  14334  shftfval  14429  2shfti  14439  prdsval  16728  pwsle  16765  sectffval  17020  sectfval  17021  isfunc  17134  isfull  17180  isfth  17184  ipoval  17764  eqgfval  18328  dvdsrval  19395  dvdsrpropd  19446  ltbval  20252  opsrval  20255  lmfval  21840  xkocnv  22422  tgphaus  22725  isphtpc  23598  bcthlem1  23927  bcth  23932  ulmval  24968  lgsquadlem3  25958  iscgrg  26298  legval  26370  ishlg  26388  perpln1  26496  perpln2  26497  isperp  26498  ishpg  26545  iscgra  26595  isinag  26624  isleag  26633  wksfval  27391  upgrtrls  27483  upgrspthswlk  27519  ajfval  28586  f1o3d  30372  f1od2  30457  inftmrel  30809  isinftm  30810  metidval  31130  faeval  31505  eulerpartlemgvv  31634  eulerpart  31640  afsval  31942  satf  32600  satfvsuc  32608  satfv1  32610  satf0suc  32623  sat1el2xp  32626  fmlasuc0  32631  bj-imdirval  34475  bj-imdirval2  34476  bj-imdirid  34478  cureq  34883  curf  34885  curunc  34889  fnopabeqd  35010  cosseq  35686  lcvfbr  36171  cmtfvalN  36361  cvrfval  36419  dicffval  38325  dicfval  38326  dicval  38327  prjspval  39302  prjspnval2  39316  0prjspn  39319  dnwech  39697  aomclem8  39710  rfovcnvfvd  40402  fsovrfovd  40404  dfafn5a  43408  sprsymrelfv  43705  sprsymrelfo  43708  upwlksfval  44059