Theorem opabbidv 5158

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540  ∃wex 1780  {cab 2713  ⟨cop 4579  {copab 5154

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-opab 5155

This theorem is referenced by:  opabbii  5159  mpteq12dva  5181  csbopab  5499  csbopabgALT  5500  csbmpt12  5501  xpeq1  5634  xpeq2  5641  opabbi2dv  5791  csbcnvgALT  5826  resopab2  5976  mptcnv  6078  cores  6187  xpco  6227  dffn5  6884  f1oiso2  7279  fvmptopab  7391  fvmptopabOLD  7392  f1ocnvd  7582  ofreq  7599  mptmpoopabbrd  7989  mptmpoopabbrdOLD  7991  bropopvvv  7998  bropfvvvv  8000  fnwelem  8039  sprmpod  8110  mpocurryd  8155  wemapwe  9554  ttrcleq  9566  xpcogend  14784  shftfval  14880  2shfti  14890  prdsval  17263  pwsle  17300  sectffval  17559  sectfval  17560  isfunc  17676  isfull  17723  isfth  17727  ipoval  18345  eqgfval  18900  dvdsrval  19982  dvdsrpropd  20033  ltbval  21350  opsrval  21353  lmfval  22489  xkocnv  23071  tgphaus  23374  isphtpc  24263  bcthlem1  24594  bcth  24599  ulmval  25645  lgsquadlem3  26636  iscgrg  27162  legval  27234  ishlg  27252  perpln1  27360  perpln2  27361  isperp  27362  ishpg  27409  iscgra  27459  isinag  27488  isleag  27497  wksfval  28265  upgrtrls  28357  upgrspthswlk  28394  ajfval  29459  f1o3d  31249  f1od2  31343  mgcoval  31551  inftmrel  31721  isinftm  31722  quslsm  31890  idlsrgval  31945  metidval  32138  faeval  32512  eulerpartlemgvv  32643  eulerpart  32649  afsval  32951  satf  33614  satfvsuc  33622  satfv1  33624  satf0suc  33637  sat1el2xp  33640  fmlasuc0  33645  bj-imdirvallem  35464  bj-imdirval2  35467  bj-imdirco  35474  bj-iminvval2  35478  cureq  35866  curf  35868  curunc  35872  fnopabeqd  35991  cosseq  36701  lcvfbr  37295  cmtfvalN  37485  cvrfval  37543  dicffval  39450  dicfval  39451  dicval  39452  prjspval  40710  prjspnerlem  40724  0prjspn  40735  dnwech  41144  aomclem8  41157  rfovcnvfvd  41944  fsovrfovd  41946  dfafn5a  45011  sprsymrelfv  45305  sprsymrelfo  45308  upwlksfval  45656