Theorem opabbidv 5166

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 631	. . . 4 ⊢ (𝜑 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
3	2	2exbidv 1926	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
4	3	abbidv 2803	. 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)})
5		df-opab 5163	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)}
6		df-opab 5163	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)}
7	4, 5, 6	3eqtr4g 2797	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781  {cab 2715  ⟨cop 4588  {copab 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-opab 5163

This theorem is referenced by:  opabbii  5167  mpteq12dva  5186  csbopab  5511  csbopabgALT  5512  csbmpt12  5513  xpeq1  5646  xpeq2  5653  opabbi2dv  5806  csbcnvgALT  5841  resopab2  6003  mptcnv  6104  cores  6215  xpco  6255  dffn5  6900  f1oiso2  7308  fvmptopab  7423  f1ocnvd  7619  ofreq  7636  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  bropopvvv  8042  bropfvvvv  8044  fnwelem  8083  sprmpod  8176  mpocurryd  8221  wemapwe  9618  ttrcleq  9630  xpcogend  14909  shftfval  15005  2shfti  15015  prdsval  17387  pwsle  17425  sectffval  17686  sectfval  17687  isfunc  17800  isfull  17848  isfth  17852  ipoval  18465  eqgfval  19117  eqg0subg  19137  dvdsrval  20309  dvdsrpropd  20364  ltbval  22010  opsrval  22013  lmfval  23188  xkocnv  23770  tgphaus  24073  isphtpc  24961  bcthlem1  25292  bcth  25297  dvcnp2  25889  dvmulbr  25909  dvcobr  25917  cmvth  25963  dvfsumle  25994  dvfsumlem2  26001  taylthlem2  26350  ulmval  26357  lgsquadlem3  27361  iscgrg  28596  legval  28668  ishlg  28686  perpln1  28794  perpln2  28795  isperp  28796  ishpg  28843  iscgra  28893  isinag  28922  isleag  28931  wksfval  29695  upgrtrls  29785  upgrspthswlk  29823  ajfval  30896  f1o3d  32715  f1od2  32808  mgcoval  33078  inftmrel  33273  isinftm  33274  erlval  33351  rlocval  33352  quslsm  33497  idlsrgval  33595  metidval  34067  faeval  34423  eulerpartlemgvv  34553  eulerpart  34559  afsval  34848  satf  35566  satfvsuc  35574  satfv1  35576  satf0suc  35589  sat1el2xp  35592  fmlasuc0  35597  bj-imdirvallem  37429  bj-imdirval2  37432  bj-imdirco  37439  bj-iminvval2  37443  cureq  37841  curf  37843  curunc  37847  fnopabeqd  37966  ecxrncnvep  38654  cosseq  38761  lcvfbr  39390  cmtfvalN  39580  cvrfval  39638  dicffval  41544  dicfval  41545  dicval  41546  prjspval  42955  prjspnerlem  42969  0prjspn  42980  dnwech  43399  aomclem8  43412  tfsconcatun  43688  tfsconcat0i  43696  tfsconcatrev  43699  rfovcnvfvd  44357  fsovrfovd  44359  dfafn5a  47514  sprsymrelfv  47848  sprsymrelfo  47851  upwlksfval  48489  sectpropdlem  49389  upfval  49529  upfval2  49530  upfval3  49531  uppropd  49534