Theorem opabbidv 5209

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  {cab 2714  ⟨cop 4632  {copab 5205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-opab 5206

This theorem is referenced by:  opabbii  5210  mpteq12dva  5231  csbopab  5560  csbopabgALT  5561  csbmpt12  5562  xpeq1  5699  xpeq2  5706  opabbi2dv  5860  csbcnvgALT  5895  resopab2  6054  mptcnv  6159  cores  6269  xpco  6309  dffn5  6967  f1oiso2  7372  fvmptopab  7487  fvmptopabOLD  7488  f1ocnvd  7684  ofreq  7701  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabbrdOLDOLD  8108  bropopvvv  8115  bropfvvvv  8117  fnwelem  8156  sprmpod  8249  mpocurryd  8294  wemapwe  9737  ttrcleq  9749  xpcogend  15013  shftfval  15109  2shfti  15119  prdsval  17500  pwsle  17537  sectffval  17794  sectfval  17795  isfunc  17909  isfull  17957  isfth  17961  ipoval  18575  eqgfval  19194  eqg0subg  19214  dvdsrval  20361  dvdsrpropd  20416  ltbval  22061  opsrval  22064  lmfval  23240  xkocnv  23822  tgphaus  24125  isphtpc  25026  bcthlem1  25358  bcth  25363  dvcnp2  25955  dvmulbr  25975  dvcobr  25983  cmvth  26029  dvfsumle  26060  dvfsumlem2  26067  taylthlem2  26416  ulmval  26423  lgsquadlem3  27426  iscgrg  28520  legval  28592  ishlg  28610  perpln1  28718  perpln2  28719  isperp  28720  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  wksfval  29627  upgrtrls  29719  upgrspthswlk  29758  ajfval  30828  f1o3d  32637  f1od2  32732  mgcoval  32976  inftmrel  33187  isinftm  33188  erlval  33262  rlocval  33263  quslsm  33433  idlsrgval  33531  metidval  33889  faeval  34247  eulerpartlemgvv  34378  eulerpart  34384  afsval  34686  satf  35358  satfvsuc  35366  satfv1  35368  satf0suc  35381  sat1el2xp  35384  fmlasuc0  35389  bj-imdirvallem  37181  bj-imdirval2  37184  bj-imdirco  37191  bj-iminvval2  37195  cureq  37603  curf  37605  curunc  37609  fnopabeqd  37728  cosseq  38427  lcvfbr  39021  cmtfvalN  39211  cvrfval  39269  dicffval  41176  dicfval  41177  dicval  41178  prjspval  42613  prjspnerlem  42627  0prjspn  42638  dnwech  43060  aomclem8  43073  tfsconcatun  43350  tfsconcat0i  43358  tfsconcatrev  43361  rfovcnvfvd  44020  fsovrfovd  44022  dfafn5a  47172  sprsymrelfv  47481  sprsymrelfo  47484  upwlksfval  48051  upfval  48933  upfval2  48934  upfval3  48935