Theorem opabbidv 5175

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

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

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 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-opab 5172

This theorem is used by:  opabbii  5176  mpteq12dva  5195  csbopab  5538  csbopabw  5539  csbmpt12  5540  xpeq1  5673  xpeq2  5680  opabbi2dv  5833  csbcnvgALTOLD  5872  resopab2  6036  mptcnv  6136  cores  6249  xpco  6291  dffn5  6940  f1oiso2  7357  fvmptopab  7472  f1ocnvd  7669  ofreq  7686  mptmpoopabbrd  8084  bropopvvv  8091  bropfvvvv  8093  fnwelem  8133  sprmpod  8226  mpocurryd  8271  cureq  8872  curf  8873  wemapwe  9680  ttrcleq  9692  xpcogend  15051  shftfval  15147  2shfti  15157  prdsval  17546  pwsle  17584  sectffval  17845  sectfval  17846  isfunc  17959  isfull  18007  isfth  18011  ipoval  18624  eqgfval  19307  eqg0subg  19330  dvdsrval  20508  dvdsrpropd  20563  ltbval  22265  opsrval  22268  lmfval  23463  xkocnv  24046  tgphaus  24349  isphtpc  25228  bcthlem1  25558  bcth  25563  dvcnp2  26154  dvmulbr  26173  dvcobr  26180  cmvth  26225  dvfsumle  26255  dvfsumlem2  26261  taylthlem2  26617  ulmval  26623  lgsquadlem3  27626  iscgrg  28862  legval  28934  ishlg2  28952  ishlg  28955  perpln1  29072  perpln2  29073  isperp  29074  ishpg  29124  iscgra  29203  tgaaddcpbllem2  29237  isinag  29244  isleag  29253  cgrabasimass  29265  brprlng  29303  wksfval  30077  upgrtrls  30171  upgrspthswlk  30211  ajfval  31298  f1o3d  33107  f1od2  33198  mgcoval  33434  inftmrel  33628  isinftm  33629  erlval  33706  rlocval  33707  quslsm  33842  idlsrgval  33921  metidval  34408  faeval  34765  eulerpartlemgvv  34895  eulerpart  34901  afsval  35190  satf  35940  satfvsuc  35948  satfv1  35950  satf0suc  35963  sat1el2xp  35966  fmlasuc0  35971  bj-imdirvallem  37940  bj-imdirval2  37943  bj-imdirco  37950  bj-iminvval2  37954  curunc  38364  fnopabeqd  38479  ecxrncnvep  39165  cosseq  39272  lcvfbr  39901  cmtfvalN  40091  cvrfval  40149  dicffval  42055  dicfval  42056  dicval  42057  prjspval  43457  prjspnerlem  43471  0prjspn  43482  dnwech  43897  aomclem8  43910  tfsconcatun  44186  tfsconcat0i  44194  tfsconcatrev  44197  rfovcnvfvd  44855  fsovrfovd  44857  dfafn5a  48056  sprsymrelfv  48402  sprsymrelfo  48405  upwlksfval  49059  sectpropdlem  49970  upfval  50110  upfval2  50111  upfval3  50112  uppropd  50115