Theorem opabbidv 5182

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

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

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-opab 5179

This theorem is used by:  opabbii  5183  mpteq12dva  5202  csbopab  5545  csbopabw  5546  csbmpt12  5547  xpeq1  5680  xpeq2  5687  opabbi2dv  5840  csbcnvgALTOLD  5879  resopab2  6043  mptcnv  6143  cores  6255  xpco  6297  dffn5  6946  f1oiso2  7361  fvmptopab  7478  f1ocnvd  7674  ofreq  7691  mptmpoopabbrd  8087  bropopvvv  8094  bropfvvvv  8096  fnwelem  8136  sprmpod  8229  mpocurryd  8274  wemapwe  9676  ttrcleq  9688  xpcogend  15037  shftfval  15133  2shfti  15143  prdsval  17533  pwsle  17571  sectffval  17832  sectfval  17833  isfunc  17946  isfull  17994  isfth  17998  ipoval  18611  eqgfval  19275  eqg0subg  19298  dvdsrval  20476  dvdsrpropd  20531  ltbval  22231  opsrval  22234  lmfval  23426  xkocnv  24008  tgphaus  24311  isphtpc  25190  bcthlem1  25520  bcth  25525  dvcnp2  26116  dvmulbr  26135  dvcobr  26142  cmvth  26187  dvfsumle  26217  dvfsumlem2  26223  taylthlem2  26574  ulmval  26580  lgsquadlem3  27583  iscgrg  28818  legval  28890  ishlg2  28908  ishlg  28911  perpln1  29027  perpln2  29028  isperp  29029  ishpg  29078  iscgra  29157  isinag  29192  isleag  29201  brprlng  29225  wksfval  29996  upgrtrls  30086  upgrspthswlk  30124  ajfval  31198  f1o3d  33008  f1od2  33101  mgcoval  33337  inftmrel  33531  isinftm  33532  erlval  33609  rlocval  33610  quslsm  33745  idlsrgval  33824  metidval  34311  faeval  34668  eulerpartlemgvv  34798  eulerpart  34804  afsval  35093  satf  35866  satfvsuc  35874  satfv1  35876  satf0suc  35889  sat1el2xp  35892  fmlasuc0  35897  bj-imdirvallem  37865  bj-imdirval2  37868  bj-imdirco  37875  bj-iminvval2  37879  cureq  38288  curf  38290  curunc  38294  fnopabeqd  38413  ecxrncnvep  39099  cosseq  39206  lcvfbr  39835  cmtfvalN  40025  cvrfval  40083  dicffval  41989  dicfval  41990  dicval  41991  prjspval  43376  prjspnerlem  43390  0prjspn  43401  dnwech  43816  aomclem8  43829  tfsconcatun  44105  tfsconcat0i  44113  tfsconcatrev  44116  rfovcnvfvd  44774  fsovrfovd  44776  dfafn5a  47938  sprsymrelfv  48284  sprsymrelfo  48287  upwlksfval  48941  sectpropdlem  49855  upfval  49995  upfval2  49996  upfval3  49997  uppropd  50000