Theorem opabbidv 5173

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  {cab 2707  ⟨cop 4595  {copab 5169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-opab 5170

This theorem is referenced by:  opabbii  5174  mpteq12dva  5193  csbopab  5515  csbopabgALT  5516  csbmpt12  5517  xpeq1  5652  xpeq2  5659  opabbi2dv  5813  csbcnvgALT  5848  resopab2  6007  mptcnv  6112  cores  6222  xpco  6262  dffn5  6919  f1oiso2  7327  fvmptopab  7443  fvmptopabOLD  7444  f1ocnvd  7640  ofreq  7657  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  bropopvvv  8069  bropfvvvv  8071  fnwelem  8110  sprmpod  8203  mpocurryd  8248  wemapwe  9650  ttrcleq  9662  xpcogend  14940  shftfval  15036  2shfti  15046  prdsval  17418  pwsle  17455  sectffval  17712  sectfval  17713  isfunc  17826  isfull  17874  isfth  17878  ipoval  18489  eqgfval  19108  eqg0subg  19128  dvdsrval  20270  dvdsrpropd  20325  ltbval  21950  opsrval  21953  lmfval  23119  xkocnv  23701  tgphaus  24004  isphtpc  24893  bcthlem1  25224  bcth  25229  dvcnp2  25821  dvmulbr  25841  dvcobr  25849  cmvth  25895  dvfsumle  25926  dvfsumlem2  25933  taylthlem2  26282  ulmval  26289  lgsquadlem3  27293  iscgrg  28439  legval  28511  ishlg  28529  perpln1  28637  perpln2  28638  isperp  28639  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  wksfval  29537  upgrtrls  29629  upgrspthswlk  29668  ajfval  30738  f1o3d  32551  f1od2  32644  mgcoval  32912  inftmrel  33134  isinftm  33135  erlval  33209  rlocval  33210  quslsm  33376  idlsrgval  33474  metidval  33880  faeval  34236  eulerpartlemgvv  34367  eulerpart  34373  afsval  34662  satf  35340  satfvsuc  35348  satfv1  35350  satf0suc  35363  sat1el2xp  35366  fmlasuc0  35371  bj-imdirvallem  37168  bj-imdirval2  37171  bj-imdirco  37178  bj-iminvval2  37182  cureq  37590  curf  37592  curunc  37596  fnopabeqd  37715  cosseq  38417  lcvfbr  39013  cmtfvalN  39203  cvrfval  39261  dicffval  41168  dicfval  41169  dicval  41170  prjspval  42591  prjspnerlem  42605  0prjspn  42616  dnwech  43037  aomclem8  43050  tfsconcatun  43326  tfsconcat0i  43334  tfsconcatrev  43337  rfovcnvfvd  43996  fsovrfovd  43998  dfafn5a  47161  sprsymrelfv  47495  sprsymrelfo  47498  upwlksfval  48123  sectpropdlem  49025  upfval  49165  upfval2  49166  upfval3  49167  uppropd  49170