Theorem opabbidv 5151

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781  {cab 2714  ⟨cop 4573  {copab 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-opab 5148

This theorem is referenced by:  opabbii  5152  mpteq12dva  5171  csbopab  5510  csbopabgALT  5511  csbmpt12  5512  xpeq1  5645  xpeq2  5652  opabbi2dv  5804  csbcnvgALT  5839  resopab2  6001  mptcnv  6102  cores  6213  xpco  6253  dffn5  6898  f1oiso2  7307  fvmptopab  7422  f1ocnvd  7618  ofreq  7635  mptmpoopabbrd  8033  bropopvvv  8040  bropfvvvv  8042  fnwelem  8081  sprmpod  8174  mpocurryd  8219  wemapwe  9618  ttrcleq  9630  xpcogend  14936  shftfval  15032  2shfti  15042  prdsval  17418  pwsle  17456  sectffval  17717  sectfval  17718  isfunc  17831  isfull  17879  isfth  17883  ipoval  18496  eqgfval  19151  eqg0subg  19171  dvdsrval  20341  dvdsrpropd  20396  ltbval  22021  opsrval  22024  lmfval  23197  xkocnv  23779  tgphaus  24082  isphtpc  24961  bcthlem1  25291  bcth  25296  dvcnp2  25887  dvmulbr  25906  dvcobr  25913  cmvth  25958  dvfsumle  25988  dvfsumlem2  25994  taylthlem2  26339  ulmval  26345  lgsquadlem3  27345  iscgrg  28580  legval  28652  ishlg  28670  perpln1  28778  perpln2  28779  isperp  28780  ishpg  28827  iscgra  28877  isinag  28906  isleag  28915  wksfval  29678  upgrtrls  29768  upgrspthswlk  29806  ajfval  30880  f1o3d  32699  f1od2  32792  mgcoval  33046  inftmrel  33241  isinftm  33242  erlval  33319  rlocval  33320  quslsm  33465  idlsrgval  33563  metidval  34034  faeval  34390  eulerpartlemgvv  34520  eulerpart  34526  afsval  34815  satf  35535  satfvsuc  35543  satfv1  35545  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  bj-imdirvallem  37494  bj-imdirval2  37497  bj-imdirco  37504  bj-iminvval2  37508  cureq  37917  curf  37919  curunc  37923  fnopabeqd  38042  ecxrncnvep  38730  cosseq  38837  lcvfbr  39466  cmtfvalN  39656  cvrfval  39714  dicffval  41620  dicfval  41621  dicval  41622  prjspval  43036  prjspnerlem  43050  0prjspn  43061  dnwech  43476  aomclem8  43489  tfsconcatun  43765  tfsconcat0i  43773  tfsconcatrev  43776  rfovcnvfvd  44434  fsovrfovd  44436  dfafn5a  47608  sprsymrelfv  47954  sprsymrelfo  47957  upwlksfval  48611  sectpropdlem  49511  upfval  49651  upfval2  49652  upfval3  49653  uppropd  49656