Theorem opabbidv 5164

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780  {cab 2714  ⟨cop 4586  {copab 5160

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-opab 5161

This theorem is referenced by:  opabbii  5165  mpteq12dva  5184  csbopab  5503  csbopabgALT  5504  csbmpt12  5505  xpeq1  5638  xpeq2  5645  opabbi2dv  5798  csbcnvgALT  5833  resopab2  5995  mptcnv  6096  cores  6207  xpco  6247  dffn5  6892  f1oiso2  7298  fvmptopab  7413  f1ocnvd  7609  ofreq  7626  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  bropopvvv  8032  bropfvvvv  8034  fnwelem  8073  sprmpod  8166  mpocurryd  8211  wemapwe  9606  ttrcleq  9618  xpcogend  14897  shftfval  14993  2shfti  15003  prdsval  17375  pwsle  17413  sectffval  17674  sectfval  17675  isfunc  17788  isfull  17836  isfth  17840  ipoval  18453  eqgfval  19105  eqg0subg  19125  dvdsrval  20297  dvdsrpropd  20352  ltbval  21998  opsrval  22001  lmfval  23176  xkocnv  23758  tgphaus  24061  isphtpc  24949  bcthlem1  25280  bcth  25285  dvcnp2  25877  dvmulbr  25897  dvcobr  25905  cmvth  25951  dvfsumle  25982  dvfsumlem2  25989  taylthlem2  26338  ulmval  26345  lgsquadlem3  27349  iscgrg  28584  legval  28656  ishlg  28674  perpln1  28782  perpln2  28783  isperp  28784  ishpg  28831  iscgra  28881  isinag  28910  isleag  28919  wksfval  29683  upgrtrls  29773  upgrspthswlk  29811  ajfval  30884  f1o3d  32704  f1od2  32798  mgcoval  33068  inftmrel  33262  isinftm  33263  erlval  33340  rlocval  33341  quslsm  33486  idlsrgval  33584  metidval  34047  faeval  34403  eulerpartlemgvv  34533  eulerpart  34539  afsval  34828  satf  35547  satfvsuc  35555  satfv1  35557  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  bj-imdirvallem  37381  bj-imdirval2  37384  bj-imdirco  37391  bj-iminvval2  37395  cureq  37793  curf  37795  curunc  37799  fnopabeqd  37918  ecxrncnvep  38590  cosseq  38685  lcvfbr  39276  cmtfvalN  39466  cvrfval  39524  dicffval  41430  dicfval  41431  dicval  41432  prjspval  42842  prjspnerlem  42856  0prjspn  42867  dnwech  43286  aomclem8  43299  tfsconcatun  43575  tfsconcat0i  43583  tfsconcatrev  43586  rfovcnvfvd  44244  fsovrfovd  44246  dfafn5a  47402  sprsymrelfv  47736  sprsymrelfo  47739  upwlksfval  48377  sectpropdlem  49277  upfval  49417  upfval2  49418  upfval3  49419  uppropd  49422