Theorem opabbidv 5178

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809  {cab 2741  ⟨cop 4596  {copab 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-opab 5175

This theorem is referenced by:  opabbii  5179  mpteq12dva  5198  csbopab  5542  csbopabw  5543  csbmpt12  5544  xpeq1  5677  xpeq2  5684  opabbi2dv  5837  csbcnvgALTOLD  5876  resopab2  6040  mptcnv  6140  cores  6252  xpco  6292  dffn5  6941  f1oiso2  7352  fvmptopab  7467  f1ocnvd  7663  ofreq  7680  mptmpoopabbrd  8079  bropopvvv  8086  bropfvvvv  8088  fnwelem  8128  sprmpod  8221  mpocurryd  8266  wemapwe  9667  ttrcleq  9679  xpcogend  15013  shftfval  15109  2shfti  15119  prdsval  17509  pwsle  17547  sectffval  17808  sectfval  17809  isfunc  17922  isfull  17970  isfth  17974  ipoval  18587  eqgfval  19245  eqg0subg  19268  dvdsrval  20444  dvdsrpropd  20499  ltbval  22175  opsrval  22178  lmfval  23370  xkocnv  23952  tgphaus  24255  isphtpc  25134  bcthlem1  25464  bcth  25469  dvcnp2  26060  dvmulbr  26079  dvcobr  26086  cmvth  26131  dvfsumle  26161  dvfsumlem2  26167  taylthlem2  26515  ulmval  26521  lgsquadlem3  27524  iscgrg  28759  legval  28831  ishlg2  28849  ishlg  28852  perpln1  28968  perpln2  28969  isperp  28970  ishpg  29019  iscgra  29098  isinag  29133  isleag  29142  brprlng  29166  wksfval  29937  upgrtrls  30027  upgrspthswlk  30065  ajfval  31139  f1o3d  32949  f1od2  33042  mgcoval  33284  inftmrel  33478  isinftm  33479  erlval  33556  rlocval  33557  quslsm  33692  idlsrgval  33771  metidval  34258  faeval  34614  eulerpartlemgvv  34744  eulerpart  34750  afsval  35039  satf  35823  satfvsuc  35831  satfv1  35833  satf0suc  35846  sat1el2xp  35849  fmlasuc0  35854  bj-imdirvallem  37802  bj-imdirval2  37805  bj-imdirco  37812  bj-iminvval2  37816  cureq  38225  curf  38227  curunc  38231  fnopabeqd  38350  ecxrncnvep  39036  cosseq  39143  lcvfbr  39772  cmtfvalN  39962  cvrfval  40020  dicffval  41926  dicfval  41927  dicval  41928  prjspval  43315  prjspnerlem  43329  0prjspn  43340  dnwech  43755  aomclem8  43768  tfsconcatun  44044  tfsconcat0i  44052  tfsconcatrev  44055  rfovcnvfvd  44713  fsovrfovd  44715  dfafn5a  47874  sprsymrelfv  48220  sprsymrelfo  48223  upwlksfval  48877  sectpropdlem  49791  upfval  49931  upfval2  49932  upfval3  49933  uppropd  49936