Theorem opabbidv 5145

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

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opabbidv.1	. . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi2d 636	. . . 4 ⊢ (𝜑 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
3	2	2exbidv 1931	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
4	3	abbidv 2806	. 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)})
5		df-opab 5142	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)}
6		df-opab 5142	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)}
7	4, 5, 6	3eqtr4g 2800	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786  {cab 2718  ⟨cop 4568  {copab 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-opab 5142

This theorem is referenced by:  opabbii  5146  mpteq12dva  5165  csbopab  5504  csbopabgALT  5505  csbmpt12  5506  xpeq1  5639  xpeq2  5646  opabbi2dv  5798  csbcnvgALT  5833  resopab2  5995  mptcnv  6096  cores  6207  xpco  6247  dffn5  6892  f1oiso2  7303  fvmptopab  7418  f1ocnvd  7614  ofreq  7631  mptmpoopabbrd  8029  bropopvvv  8036  bropfvvvv  8038  fnwelem  8078  sprmpod  8171  mpocurryd  8216  wemapwe  9616  ttrcleq  9628  xpcogend  14934  shftfval  15030  2shfti  15040  prdsval  17416  pwsle  17454  sectffval  17715  sectfval  17716  isfunc  17829  isfull  17877  isfth  17881  ipoval  18494  eqgfval  19149  eqg0subg  19169  dvdsrval  20339  dvdsrpropd  20394  ltbval  22026  opsrval  22029  lmfval  23222  xkocnv  23804  tgphaus  24107  isphtpc  24986  bcthlem1  25316  bcth  25321  dvcnp2  25912  dvmulbr  25931  dvcobr  25938  cmvth  25983  dvfsumle  26013  dvfsumlem2  26019  taylthlem2  26364  ulmval  26370  lgsquadlem3  27370  iscgrg  28605  legval  28677  ishlg  28695  perpln1  28803  perpln2  28804  isperp  28805  ishpg  28852  iscgra  28902  isinag  28931  isleag  28940  wksfval  29703  upgrtrls  29793  upgrspthswlk  29831  ajfval  30905  f1o3d  32725  f1od2  32818  mgcoval  33072  inftmrel  33268  isinftm  33269  erlval  33346  rlocval  33347  quslsm  33495  idlsrgval  33593  metidval  34081  faeval  34437  eulerpartlemgvv  34567  eulerpart  34573  afsval  34862  satf  35588  satfvsuc  35596  satfv1  35598  satf0suc  35611  sat1el2xp  35614  fmlasuc0  35619  bj-imdirvallem  37547  bj-imdirval2  37550  bj-imdirco  37557  bj-iminvval2  37561  cureq  37970  curf  37972  curunc  37976  fnopabeqd  38095  ecxrncnvep  38783  cosseq  38890  lcvfbr  39519  cmtfvalN  39709  cvrfval  39767  dicffval  41673  dicfval  41674  dicval  41675  prjspval  43060  prjspnerlem  43074  0prjspn  43085  dnwech  43500  aomclem8  43513  tfsconcatun  43789  tfsconcat0i  43797  tfsconcatrev  43800  rfovcnvfvd  44458  fsovrfovd  44460  dfafn5a  47630  sprsymrelfv  47976  sprsymrelfo  47979  upwlksfval  48633  sectpropdlem  49533  upfval  49673  upfval2  49674  upfval3  49675  uppropd  49678