Theorem opabbidv 5176

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781  {cab 2708  ⟨cop 4597  {copab 5172

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-opab 5173

This theorem is referenced by:  opabbii  5177  mpteq12dva  5199  csbopab  5517  csbopabgALT  5518  csbmpt12  5519  xpeq1  5652  xpeq2  5659  opabbi2dv  5810  csbcnvgALT  5845  resopab2  5995  mptcnv  6097  cores  6206  xpco  6246  dffn5  6906  f1oiso2  7302  fvmptopab  7416  fvmptopabOLD  7417  f1ocnvd  7609  ofreq  7626  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8020  bropopvvv  8027  bropfvvvv  8029  fnwelem  8068  sprmpod  8160  mpocurryd  8205  wemapwe  9642  ttrcleq  9654  xpcogend  14871  shftfval  14967  2shfti  14977  prdsval  17351  pwsle  17388  sectffval  17647  sectfval  17648  isfunc  17764  isfull  17811  isfth  17815  ipoval  18433  eqgfval  18992  dvdsrval  20088  dvdsrpropd  20141  ltbval  21481  opsrval  21484  lmfval  22620  xkocnv  23202  tgphaus  23505  isphtpc  24394  bcthlem1  24725  bcth  24730  ulmval  25776  lgsquadlem3  26767  iscgrg  27517  legval  27589  ishlg  27607  perpln1  27715  perpln2  27716  isperp  27717  ishpg  27764  iscgra  27814  isinag  27843  isleag  27852  wksfval  28620  upgrtrls  28712  upgrspthswlk  28749  ajfval  29814  f1o3d  31608  f1od2  31706  mgcoval  31916  inftmrel  32086  isinftm  32087  quslsm  32260  idlsrgval  32321  metidval  32560  faeval  32934  eulerpartlemgvv  33065  eulerpart  33071  afsval  33373  satf  34034  satfvsuc  34042  satfv1  34044  satf0suc  34057  sat1el2xp  34060  fmlasuc0  34065  bj-imdirvallem  35724  bj-imdirval2  35727  bj-imdirco  35734  bj-iminvval2  35738  cureq  36127  curf  36129  curunc  36133  fnopabeqd  36252  cosseq  36961  lcvfbr  37555  cmtfvalN  37745  cvrfval  37803  dicffval  39710  dicfval  39711  dicval  39712  prjspval  40999  prjspnerlem  41013  0prjspn  41024  dnwech  41433  aomclem8  41446  tfsconcatun  41730  tfsconcat0i  41738  tfsconcatrev  41741  rfovcnvfvd  42401  fsovrfovd  42403  dfafn5a  45512  sprsymrelfv  45806  sprsymrelfo  45809  upwlksfval  46157