Theorem opabbidv 5215

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782  {cab 2710  ⟨cop 4635  {copab 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-opab 5212

This theorem is referenced by:  opabbii  5216  mpteq12dva  5238  csbopab  5556  csbopabgALT  5557  csbmpt12  5558  xpeq1  5691  xpeq2  5698  opabbi2dv  5850  csbcnvgALT  5885  resopab2  6037  mptcnv  6140  cores  6249  xpco  6289  dffn5  6951  f1oiso2  7349  fvmptopab  7463  fvmptopabOLD  7464  f1ocnvd  7657  ofreq  7674  mptmpoopabbrd  8067  mptmpoopabbrdOLD  8069  bropopvvv  8076  bropfvvvv  8078  fnwelem  8117  sprmpod  8209  mpocurryd  8254  wemapwe  9692  ttrcleq  9704  xpcogend  14921  shftfval  15017  2shfti  15027  prdsval  17401  pwsle  17438  sectffval  17697  sectfval  17698  isfunc  17814  isfull  17861  isfth  17865  ipoval  18483  eqgfval  19056  eqg0subg  19073  dvdsrval  20175  dvdsrpropd  20230  ltbval  21598  opsrval  21601  lmfval  22736  xkocnv  23318  tgphaus  23621  isphtpc  24510  bcthlem1  24841  bcth  24846  ulmval  25892  lgsquadlem3  26885  iscgrg  27763  legval  27835  ishlg  27853  perpln1  27961  perpln2  27962  isperp  27963  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  wksfval  28866  upgrtrls  28958  upgrspthswlk  28995  ajfval  30062  f1o3d  31851  f1od2  31946  mgcoval  32156  inftmrel  32326  isinftm  32327  quslsm  32516  idlsrgval  32617  metidval  32870  faeval  33244  eulerpartlemgvv  33375  eulerpart  33381  afsval  33683  satf  34344  satfvsuc  34352  satfv1  34354  satf0suc  34367  sat1el2xp  34370  fmlasuc0  34375  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  bj-imdirvallem  36061  bj-imdirval2  36064  bj-imdirco  36071  bj-iminvval2  36075  cureq  36464  curf  36466  curunc  36470  fnopabeqd  36589  cosseq  37296  lcvfbr  37890  cmtfvalN  38080  cvrfval  38138  dicffval  40045  dicfval  40046  dicval  40047  prjspval  41345  prjspnerlem  41359  0prjspn  41370  dnwech  41790  aomclem8  41803  tfsconcatun  42087  tfsconcat0i  42095  tfsconcatrev  42098  rfovcnvfvd  42758  fsovrfovd  42760  dfafn5a  45868  sprsymrelfv  46162  sprsymrelfo  46165  upwlksfval  46513