Theorem opabbidv 5141

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787  {cab 2719  ⟨cop 4564  {copab 5137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-opab 5138

This theorem is referenced by:  opabbii  5142  mpteq12dva  5161  csbopab  5500  csbopabw  5501  csbmpt12  5502  xpeq1  5635  xpeq2  5642  opabbi2dv  5794  csbcnvgALTOLD  5833  resopab2  5995  mptcnv  6096  cores  6204  xpco  6244  dffn5  6889  f1oiso2  7300  fvmptopab  7415  f1ocnvd  7611  ofreq  7628  mptmpoopabbrd  8026  bropopvvv  8033  bropfvvvv  8035  fnwelem  8075  sprmpod  8168  mpocurryd  8213  wemapwe  9613  ttrcleq  9625  xpcogend  14931  shftfval  15027  2shfti  15037  prdsval  17413  pwsle  17451  sectffval  17712  sectfval  17713  isfunc  17826  isfull  17874  isfth  17878  ipoval  18491  eqgfval  19146  eqg0subg  19166  dvdsrval  20336  dvdsrpropd  20391  ltbval  22023  opsrval  22026  lmfval  23219  xkocnv  23801  tgphaus  24104  isphtpc  24983  bcthlem1  25313  bcth  25318  dvcnp2  25909  dvmulbr  25928  dvcobr  25935  cmvth  25980  dvfsumle  26010  dvfsumlem2  26016  taylthlem2  26361  ulmval  26367  lgsquadlem3  27367  iscgrg  28602  legval  28674  ishlg  28692  perpln1  28800  perpln2  28801  isperp  28802  ishpg  28849  iscgra  28899  isinag  28928  isleag  28937  wksfval  29700  upgrtrls  29790  upgrspthswlk  29828  ajfval  30902  f1o3d  32722  f1od2  32815  mgcoval  33069  inftmrel  33265  isinftm  33266  erlval  33343  rlocval  33344  quslsm  33492  idlsrgval  33598  metidval  34086  faeval  34442  eulerpartlemgvv  34572  eulerpart  34578  afsval  34870  satf  35596  satfvsuc  35604  satfv1  35606  satf0suc  35619  sat1el2xp  35622  fmlasuc0  35627  bj-imdirvallem  37555  bj-imdirval2  37558  bj-imdirco  37565  bj-iminvval2  37569  cureq  37978  curf  37980  curunc  37984  fnopabeqd  38103  ecxrncnvep  38791  cosseq  38898  lcvfbr  39527  cmtfvalN  39717  cvrfval  39775  dicffval  41681  dicfval  41682  dicval  41683  prjspval  43068  prjspnerlem  43082  0prjspn  43093  dnwech  43508  aomclem8  43521  tfsconcatun  43797  tfsconcat0i  43805  tfsconcatrev  43808  rfovcnvfvd  44466  fsovrfovd  44468  dfafn5a  47637  sprsymrelfv  47983  sprsymrelfo  47986  upwlksfval  48640  sectpropdlem  49540  upfval  49680  upfval2  49681  upfval3  49682  uppropd  49685