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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802  {cab 2743  ⟨cop 4591  {copab 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-opab 5168

This theorem is referenced by:  opabbii  5172  mpteq12dva  5191  csbopab  5531  csbopabw  5532  csbmpt12  5533  xpeq1  5666  xpeq2  5673  opabbi2dv  5826  csbcnvgALTOLD  5865  resopab2  6029  mptcnv  6129  cores  6240  xpco  6280  dffn5  6929  f1oiso2  7340  fvmptopab  7455  f1ocnvd  7651  ofreq  7668  mptmpoopabbrd  8066  bropopvvv  8073  bropfvvvv  8075  fnwelem  8115  sprmpod  8208  mpocurryd  8253  wemapwe  9654  ttrcleq  9666  xpcogend  15001  shftfval  15097  2shfti  15107  prdsval  17498  pwsle  17536  sectffval  17797  sectfval  17798  isfunc  17911  isfull  17959  isfth  17963  ipoval  18576  eqgfval  19235  eqg0subg  19258  dvdsrval  20434  dvdsrpropd  20489  ltbval  22154  opsrval  22157  lmfval  23350  xkocnv  23932  tgphaus  24235  isphtpc  25114  bcthlem1  25444  bcth  25449  dvcnp2  26040  dvmulbr  26059  dvcobr  26066  cmvth  26111  dvfsumle  26141  dvfsumlem2  26147  taylthlem2  26495  ulmval  26501  lgsquadlem3  27504  iscgrg  28739  legval  28811  ishlg  28829  perpln1  28941  perpln2  28942  isperp  28943  ishpg  28990  iscgra  29061  isinag  29090  isleag  29099  brprlng  29123  wksfval  29868  upgrtrls  29958  upgrspthswlk  29996  ajfval  31070  f1o3d  32883  f1od2  32976  mgcoval  33219  inftmrel  33413  isinftm  33414  erlval  33491  rlocval  33492  quslsm  33630  idlsrgval  33710  metidval  34197  faeval  34553  eulerpartlemgvv  34683  eulerpart  34689  afsval  34978  satf  35716  satfvsuc  35724  satfv1  35726  satf0suc  35739  sat1el2xp  35742  fmlasuc0  35747  bj-imdirvallem  37684  bj-imdirval2  37687  bj-imdirco  37694  bj-iminvval2  37698  cureq  38107  curf  38109  curunc  38113  fnopabeqd  38232  ecxrncnvep  38920  cosseq  39027  lcvfbr  39656  cmtfvalN  39846  cvrfval  39904  dicffval  41810  dicfval  41811  dicval  41812  prjspval  43197  prjspnerlem  43211  0prjspn  43222  dnwech  43637  aomclem8  43650  tfsconcatun  43926  tfsconcat0i  43934  tfsconcatrev  43937  rfovcnvfvd  44595  fsovrfovd  44597  dfafn5a  47752  sprsymrelfv  48098  sprsymrelfo  48101  upwlksfval  48755  sectpropdlem  49665  upfval  49805  upfval2  49806  upfval3  49807  uppropd  49810