Theorem opabbidv 5136

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783  {cab 2715  ⟨cop 4564  {copab 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-opab 5133

This theorem is referenced by:  opabbii  5137  mpteq12dva  5159  csbopab  5461  csbopabgALT  5462  csbmpt12  5463  xpeq1  5594  xpeq2  5601  opabbi2dv  5747  csbcnvgALT  5782  resopab2  5933  mptcnv  6032  cores  6142  xpco  6181  dffn5  6810  f1oiso2  7203  fvmptopab  7308  f1ocnvd  7498  ofreq  7515  mptmpoopabbrd  7894  bropopvvv  7901  bropfvvvv  7903  fnwelem  7943  sprmpod  8011  mpocurryd  8056  wemapwe  9385  xpcogend  14613  shftfval  14709  2shfti  14719  prdsval  17083  pwsle  17120  sectffval  17379  sectfval  17380  isfunc  17495  isfull  17542  isfth  17546  ipoval  18163  eqgfval  18719  dvdsrval  19802  dvdsrpropd  19853  ltbval  21154  opsrval  21157  lmfval  22291  xkocnv  22873  tgphaus  23176  isphtpc  24063  bcthlem1  24393  bcth  24398  ulmval  25444  lgsquadlem3  26435  iscgrg  26777  legval  26849  ishlg  26867  perpln1  26975  perpln2  26976  isperp  26977  ishpg  27024  iscgra  27074  isinag  27103  isleag  27112  wksfval  27879  upgrtrls  27971  upgrspthswlk  28007  ajfval  29072  f1o3d  30863  f1od2  30958  mgcoval  31166  inftmrel  31336  isinftm  31337  quslsm  31495  idlsrgval  31550  metidval  31742  faeval  32114  eulerpartlemgvv  32243  eulerpart  32249  afsval  32551  satf  33215  satfvsuc  33223  satfv1  33225  satf0suc  33238  sat1el2xp  33241  fmlasuc0  33246  ttrcleq  33695  bj-imdirvallem  35278  bj-imdirval2  35281  bj-imdirco  35288  bj-iminvval2  35292  cureq  35680  curf  35682  curunc  35686  fnopabeqd  35805  cosseq  36476  lcvfbr  36961  cmtfvalN  37151  cvrfval  37209  dicffval  39115  dicfval  39116  dicval  39117  prjspval  40363  prjspnerlem  40377  0prjspn  40386  dnwech  40789  aomclem8  40802  rfovcnvfvd  41504  fsovrfovd  41506  dfafn5a  44539  sprsymrelfv  44834  sprsymrelfo  44837  upwlksfval  45185