Theorem opabbidv 5165

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559  ∃wex 1798  {cab 2739  ⟨cop 4587  {copab 5161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-opab 5162

This theorem is referenced by:  opabbii  5166  mpteq12dva  5185  csbopab  5524  csbopabw  5525  csbmpt12  5526  xpeq1  5659  xpeq2  5666  opabbi2dv  5819  csbcnvgALTOLD  5858  resopab2  6022  mptcnv  6122  cores  6232  xpco  6272  dffn5  6921  f1oiso2  7332  fvmptopab  7447  f1ocnvd  7643  ofreq  7660  mptmpoopabbrd  8057  bropopvvv  8064  bropfvvvv  8066  fnwelem  8106  sprmpod  8199  mpocurryd  8244  wemapwe  9649  ttrcleq  9661  xpcogend  14984  shftfval  15080  2shfti  15090  prdsval  17467  pwsle  17505  sectffval  17766  sectfval  17767  isfunc  17880  isfull  17928  isfth  17932  ipoval  18545  eqgfval  19200  eqg0subg  19220  dvdsrval  20389  dvdsrpropd  20444  ltbval  22076  opsrval  22079  lmfval  23272  xkocnv  23854  tgphaus  24157  isphtpc  25036  bcthlem1  25366  bcth  25371  dvcnp2  25962  dvmulbr  25981  dvcobr  25988  cmvth  26033  dvfsumle  26063  dvfsumlem2  26069  taylthlem2  26414  ulmval  26420  lgsquadlem3  27423  iscgrg  28658  legval  28730  ishlg  28748  perpln1  28856  perpln2  28857  isperp  28858  ishpg  28905  iscgra  28955  isinag  28984  isleag  28993  wksfval  29756  upgrtrls  29846  upgrspthswlk  29884  ajfval  30958  f1o3d  32778  f1od2  32871  mgcoval  33125  inftmrel  33321  isinftm  33322  erlval  33400  rlocval  33401  quslsm  33552  idlsrgval  33660  metidval  34148  faeval  34504  eulerpartlemgvv  34634  eulerpart  34640  afsval  34932  satf  35667  satfvsuc  35675  satfv1  35677  satf0suc  35690  sat1el2xp  35693  fmlasuc0  35698  bj-imdirvallem  37636  bj-imdirval2  37639  bj-imdirco  37646  bj-iminvval2  37650  cureq  38059  curf  38061  curunc  38065  fnopabeqd  38184  ecxrncnvep  38872  cosseq  38979  lcvfbr  39608  cmtfvalN  39798  cvrfval  39856  dicffval  41762  dicfval  41763  dicval  41764  prjspval  43149  prjspnerlem  43163  0prjspn  43174  dnwech  43589  aomclem8  43602  tfsconcatun  43878  tfsconcat0i  43886  tfsconcatrev  43889  rfovcnvfvd  44547  fsovrfovd  44549  dfafn5a  47718  sprsymrelfv  48064  sprsymrelfo  48067  upwlksfval  48721  sectpropdlem  49621  upfval  49761  upfval2  49762  upfval3  49763  uppropd  49766