Theorem opabbidv 5159

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780  {cab 2711  ⟨cop 4581  {copab 5155

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-opab 5156

This theorem is referenced by:  opabbii  5160  mpteq12dva  5179  csbopab  5498  csbopabgALT  5499  csbmpt12  5500  xpeq1  5633  xpeq2  5640  opabbi2dv  5793  csbcnvgALT  5828  resopab2  5989  mptcnv  6090  cores  6201  xpco  6241  dffn5  6886  f1oiso2  7292  fvmptopab  7407  f1ocnvd  7603  ofreq  7620  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8019  bropopvvv  8026  bropfvvvv  8028  fnwelem  8067  sprmpod  8160  mpocurryd  8205  wemapwe  9594  ttrcleq  9606  xpcogend  14883  shftfval  14979  2shfti  14989  prdsval  17361  pwsle  17398  sectffval  17659  sectfval  17660  isfunc  17773  isfull  17821  isfth  17825  ipoval  18438  eqgfval  19090  eqg0subg  19110  dvdsrval  20281  dvdsrpropd  20336  ltbval  21979  opsrval  21982  lmfval  23148  xkocnv  23730  tgphaus  24033  isphtpc  24921  bcthlem1  25252  bcth  25257  dvcnp2  25849  dvmulbr  25869  dvcobr  25877  cmvth  25923  dvfsumle  25954  dvfsumlem2  25961  taylthlem2  26310  ulmval  26317  lgsquadlem3  27321  iscgrg  28491  legval  28563  ishlg  28581  perpln1  28689  perpln2  28690  isperp  28691  ishpg  28738  iscgra  28788  isinag  28817  isleag  28826  wksfval  29590  upgrtrls  29680  upgrspthswlk  29718  ajfval  30791  f1o3d  32610  f1od2  32706  mgcoval  32974  inftmrel  33156  isinftm  33157  erlval  33232  rlocval  33233  quslsm  33377  idlsrgval  33475  metidval  33924  faeval  34280  eulerpartlemgvv  34410  eulerpart  34416  afsval  34705  satf  35418  satfvsuc  35426  satfv1  35428  satf0suc  35441  sat1el2xp  35444  fmlasuc0  35449  bj-imdirvallem  37245  bj-imdirval2  37248  bj-imdirco  37255  bj-iminvval2  37259  cureq  37656  curf  37658  curunc  37662  fnopabeqd  37781  ecxrncnvep  38453  cosseq  38548  lcvfbr  39139  cmtfvalN  39329  cvrfval  39387  dicffval  41293  dicfval  41294  dicval  41295  prjspval  42721  prjspnerlem  42735  0prjspn  42746  dnwech  43165  aomclem8  43178  tfsconcatun  43454  tfsconcat0i  43462  tfsconcatrev  43465  rfovcnvfvd  44124  fsovrfovd  44126  dfafn5a  47284  sprsymrelfv  47618  sprsymrelfo  47621  upwlksfval  48259  sectpropdlem  49161  upfval  49301  upfval2  49302  upfval3  49303  uppropd  49306