Theorem opabbidv 5171

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812  {cab 2739  ⟨cop 4590  {copab 5167

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-opab 5168

This theorem is used by:  opabbii  5172  mpteq12dva  5191  csbopab  5530  csbopabw  5531  csbmpt12  5532  xpeq1  5665  xpeq2  5672  opabbi2dv  5827  csbcnvgALTOLD  5866  resopab2  6030  mptcnv  6130  cores  6243  xpco  6285  dffn5  6935  f1oiso2  7352  fvmptopab  7467  f1ocnvd  7664  mpt3eqdv  7678  ofreq  7686  mptmpoopabbrd  8083  bropopvvv  8090  bropfvvvv  8092  fnwelem  8132  sprmpod  8225  mpocurryd  8270  cureq  8873  curf  8874  wemapwe  9682  ttrcleq  9694  xpcogend  15107  shftfval  15203  2shfti  15213  prdsval  17606  pwsle  17644  sectffval  17905  sectfval  17906  isfunc  18019  isfull  18067  isfth  18071  ipoval  18684  eqgfval  19368  eqg0subg  19391  dvdsrval  20571  dvdsrpropd  20626  ltbval  22332  opsrval  22335  lmfval  23530  xkocnv  24113  tgphaus  24416  isphtpc  25295  bcthlem1  25625  bcth  25630  dvcnp2  26220  dvmulbr  26239  dvcobr  26246  cmvth  26291  dvfsumle  26321  dvfsumlem2  26327  taylthlem2  26683  ulmval  26689  lgsquadlem3  27691  iscgrg  28957  legval  29029  ishlg2  29047  ishlg  29050  perpln1  29167  perpln2  29168  isperp  29169  ishpg  29219  iscgra  29298  tgaaddcpbllem2  29332  isinag  29339  isleag  29348  cgrabasimass  29360  brprlng  29398  wksfval  30172  upgrtrls  30266  upgrspthswlk  30306  ajfval  31393  f1o3d  33202  f1od2  33293  mgcoval  33529  inftmrel  33723  isinftm  33724  erlval  33801  rlocval  33802  quslsm  33938  idlsrgval  34017  metidval  34504  faeval  34861  eulerpartlemgvv  34991  eulerpart  34997  afsval  35286  satf  36087  satfvsuc  36095  satfv1  36097  satf0suc  36110  sat1el2xp  36113  fmlasuc0  36118  bj-imdirvallem  38069  bj-imdirval2  38072  bj-imdirco  38079  bj-iminvval2  38083  curunc  38493  fnopabeqd  38623  ecxrncnvep  39309  cosseq  39416  lcvfbr  40045  cmtfvalN  40235  cvrfval  40293  dicffval  42199  dicfval  42200  dicval  42201  prjspval  43593  prjspnerlem  43607  0prjspn  43618  dnwech  44008  aomclem8  44021  tfsconcatun  44297  tfsconcat0i  44305  tfsconcatrev  44308  rfovcnvfvd  44966  fsovrfovd  44968  dfafn5a  48174  sprsymrelfv  48520  sprsymrelfo  48523  upwlksfval  49177  sectpropdlem  50088  upfval  50228  upfval2  50229  upfval3  50230  uppropd  50233