Theorem opabbidv 5155

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780  {cab 2708  ⟨cop 4580  {copab 5151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-opab 5152

This theorem is referenced by:  opabbii  5156  mpteq12dva  5175  csbopab  5493  csbopabgALT  5494  csbmpt12  5495  xpeq1  5628  xpeq2  5635  opabbi2dv  5787  csbcnvgALT  5822  resopab2  5982  mptcnv  6083  cores  6193  xpco  6232  dffn5  6875  f1oiso2  7281  fvmptopab  7396  f1ocnvd  7592  ofreq  7609  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  bropopvvv  8015  bropfvvvv  8017  fnwelem  8056  sprmpod  8149  mpocurryd  8194  wemapwe  9582  ttrcleq  9594  xpcogend  14873  shftfval  14969  2shfti  14979  prdsval  17351  pwsle  17388  sectffval  17649  sectfval  17650  isfunc  17763  isfull  17811  isfth  17815  ipoval  18428  eqgfval  19081  eqg0subg  19101  dvdsrval  20272  dvdsrpropd  20327  ltbval  21971  opsrval  21974  lmfval  23140  xkocnv  23722  tgphaus  24025  isphtpc  24913  bcthlem1  25244  bcth  25249  dvcnp2  25841  dvmulbr  25861  dvcobr  25869  cmvth  25915  dvfsumle  25946  dvfsumlem2  25953  taylthlem2  26302  ulmval  26309  lgsquadlem3  27313  iscgrg  28483  legval  28555  ishlg  28573  perpln1  28681  perpln2  28682  isperp  28683  ishpg  28730  iscgra  28780  isinag  28809  isleag  28818  wksfval  29581  upgrtrls  29671  upgrspthswlk  29709  ajfval  30779  f1o3d  32598  f1od2  32692  mgcoval  32957  inftmrel  33139  isinftm  33140  erlval  33215  rlocval  33216  quslsm  33360  idlsrgval  33458  metidval  33893  faeval  34249  eulerpartlemgvv  34379  eulerpart  34385  afsval  34674  satf  35365  satfvsuc  35373  satfv1  35375  satf0suc  35388  sat1el2xp  35391  fmlasuc0  35396  bj-imdirvallem  37193  bj-imdirval2  37196  bj-imdirco  37203  bj-iminvval2  37207  cureq  37615  curf  37617  curunc  37621  fnopabeqd  37740  cosseq  38442  lcvfbr  39038  cmtfvalN  39228  cvrfval  39286  dicffval  41192  dicfval  41193  dicval  41194  prjspval  42615  prjspnerlem  42629  0prjspn  42640  dnwech  43060  aomclem8  43073  tfsconcatun  43349  tfsconcat0i  43357  tfsconcatrev  43360  rfovcnvfvd  44019  fsovrfovd  44021  dfafn5a  47170  sprsymrelfv  47504  sprsymrelfo  47507  upwlksfval  48145  sectpropdlem  49047  upfval  49187  upfval2  49188  upfval3  49189  uppropd  49192