Theorem opabbidv 5176

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  {cab 2708  ⟨cop 4598  {copab 5172

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-opab 5173

This theorem is referenced by:  opabbii  5177  mpteq12dva  5196  csbopab  5518  csbopabgALT  5519  csbmpt12  5520  xpeq1  5655  xpeq2  5662  opabbi2dv  5816  csbcnvgALT  5851  resopab2  6010  mptcnv  6115  cores  6225  xpco  6265  dffn5  6922  f1oiso2  7330  fvmptopab  7446  fvmptopabOLD  7447  f1ocnvd  7643  ofreq  7660  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabbrdOLDOLD  8065  bropopvvv  8072  bropfvvvv  8074  fnwelem  8113  sprmpod  8206  mpocurryd  8251  wemapwe  9657  ttrcleq  9669  xpcogend  14947  shftfval  15043  2shfti  15053  prdsval  17425  pwsle  17462  sectffval  17719  sectfval  17720  isfunc  17833  isfull  17881  isfth  17885  ipoval  18496  eqgfval  19115  eqg0subg  19135  dvdsrval  20277  dvdsrpropd  20332  ltbval  21957  opsrval  21960  lmfval  23126  xkocnv  23708  tgphaus  24011  isphtpc  24900  bcthlem1  25231  bcth  25236  dvcnp2  25828  dvmulbr  25848  dvcobr  25856  cmvth  25902  dvfsumle  25933  dvfsumlem2  25940  taylthlem2  26289  ulmval  26296  lgsquadlem3  27300  iscgrg  28446  legval  28518  ishlg  28536  perpln1  28644  perpln2  28645  isperp  28646  ishpg  28693  iscgra  28743  isinag  28772  isleag  28781  wksfval  29544  upgrtrls  29636  upgrspthswlk  29675  ajfval  30745  f1o3d  32558  f1od2  32651  mgcoval  32919  inftmrel  33141  isinftm  33142  erlval  33216  rlocval  33217  quslsm  33383  idlsrgval  33481  metidval  33887  faeval  34243  eulerpartlemgvv  34374  eulerpart  34380  afsval  34669  satf  35347  satfvsuc  35355  satfv1  35357  satf0suc  35370  sat1el2xp  35373  fmlasuc0  35378  bj-imdirvallem  37175  bj-imdirval2  37178  bj-imdirco  37185  bj-iminvval2  37189  cureq  37597  curf  37599  curunc  37603  fnopabeqd  37722  cosseq  38424  lcvfbr  39020  cmtfvalN  39210  cvrfval  39268  dicffval  41175  dicfval  41176  dicval  41177  prjspval  42598  prjspnerlem  42612  0prjspn  42623  dnwech  43044  aomclem8  43057  tfsconcatun  43333  tfsconcat0i  43341  tfsconcatrev  43344  rfovcnvfvd  44003  fsovrfovd  44005  dfafn5a  47165  sprsymrelfv  47499  sprsymrelfo  47502  upwlksfval  48127  sectpropdlem  49029  upfval  49169  upfval2  49170  upfval3  49171  uppropd  49174