Theorem opabbidv 5141

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782  {cab 2716  ⟨cop 4568  {copab 5137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-opab 5138

This theorem is referenced by:  opabbii  5142  mpteq12dva  5164  csbopab  5469  csbopabgALT  5470  csbmpt12  5471  xpeq1  5604  xpeq2  5611  opabbi2dv  5761  csbcnvgALT  5796  resopab2  5947  mptcnv  6048  cores  6157  xpco  6196  dffn5  6837  f1oiso2  7232  fvmptopab  7338  fvmptopabOLD  7339  f1ocnvd  7529  ofreq  7546  mptmpoopabbrd  7930  mptmpoopabbrdOLD  7932  bropopvvv  7939  bropfvvvv  7941  fnwelem  7981  sprmpod  8049  mpocurryd  8094  wemapwe  9464  ttrcleq  9476  xpcogend  14694  shftfval  14790  2shfti  14800  prdsval  17175  pwsle  17212  sectffval  17471  sectfval  17472  isfunc  17588  isfull  17635  isfth  17639  ipoval  18257  eqgfval  18813  dvdsrval  19896  dvdsrpropd  19947  ltbval  21253  opsrval  21256  lmfval  22392  xkocnv  22974  tgphaus  23277  isphtpc  24166  bcthlem1  24497  bcth  24502  ulmval  25548  lgsquadlem3  26539  iscgrg  26882  legval  26954  ishlg  26972  perpln1  27080  perpln2  27081  isperp  27082  ishpg  27129  iscgra  27179  isinag  27208  isleag  27217  wksfval  27985  upgrtrls  28078  upgrspthswlk  28115  ajfval  29180  f1o3d  30971  f1od2  31065  mgcoval  31273  inftmrel  31443  isinftm  31444  quslsm  31602  idlsrgval  31657  metidval  31849  faeval  32223  eulerpartlemgvv  32352  eulerpart  32358  afsval  32660  satf  33324  satfvsuc  33332  satfv1  33334  satf0suc  33347  sat1el2xp  33350  fmlasuc0  33355  bj-imdirvallem  35360  bj-imdirval2  35363  bj-imdirco  35370  bj-iminvval2  35374  cureq  35762  curf  35764  curunc  35768  fnopabeqd  35887  cosseq  36556  lcvfbr  37041  cmtfvalN  37231  cvrfval  37289  dicffval  39195  dicfval  39196  dicval  39197  prjspval  40449  prjspnerlem  40463  0prjspn  40472  dnwech  40880  aomclem8  40893  rfovcnvfvd  41622  fsovrfovd  41624  dfafn5a  44663  sprsymrelfv  44957  sprsymrelfo  44960  upwlksfval  45308