Theorem opabbidv 5213

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536  ∃wex 1775  {cab 2711  ⟨cop 4636  {copab 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-opab 5210

This theorem is referenced by:  opabbii  5214  mpteq12dva  5236  csbopab  5564  csbopabgALT  5565  csbmpt12  5566  xpeq1  5702  xpeq2  5709  opabbi2dv  5862  csbcnvgALT  5897  resopab2  6055  mptcnv  6161  cores  6270  xpco  6310  dffn5  6966  f1oiso2  7371  fvmptopab  7486  fvmptopabOLD  7487  f1ocnvd  7683  ofreq  7700  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  bropopvvv  8113  bropfvvvv  8115  fnwelem  8154  sprmpod  8247  mpocurryd  8292  wemapwe  9734  ttrcleq  9746  xpcogend  15009  shftfval  15105  2shfti  15115  prdsval  17501  pwsle  17538  sectffval  17797  sectfval  17798  isfunc  17914  isfull  17963  isfth  17967  ipoval  18587  eqgfval  19206  eqg0subg  19226  dvdsrval  20377  dvdsrpropd  20432  ltbval  22078  opsrval  22081  lmfval  23255  xkocnv  23837  tgphaus  24140  isphtpc  25039  bcthlem1  25371  bcth  25376  dvcnp2  25969  dvmulbr  25989  dvcobr  25997  cmvth  26043  dvfsumle  26074  dvfsumlem2  26081  taylthlem2  26430  ulmval  26437  lgsquadlem3  27440  iscgrg  28534  legval  28606  ishlg  28624  perpln1  28732  perpln2  28733  isperp  28734  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  wksfval  29641  upgrtrls  29733  upgrspthswlk  29770  ajfval  30837  f1o3d  32643  f1od2  32738  mgcoval  32960  inftmrel  33169  isinftm  33170  erlval  33244  rlocval  33245  quslsm  33412  idlsrgval  33510  metidval  33850  faeval  34226  eulerpartlemgvv  34357  eulerpart  34363  afsval  34664  satf  35337  satfvsuc  35345  satfv1  35347  satf0suc  35360  sat1el2xp  35363  fmlasuc0  35368  bj-imdirvallem  37162  bj-imdirval2  37165  bj-imdirco  37172  bj-iminvval2  37176  cureq  37582  curf  37584  curunc  37588  fnopabeqd  37707  cosseq  38407  lcvfbr  39001  cmtfvalN  39191  cvrfval  39249  dicffval  41156  dicfval  41157  dicval  41158  prjspval  42589  prjspnerlem  42603  0prjspn  42614  dnwech  43036  aomclem8  43049  tfsconcatun  43326  tfsconcat0i  43334  tfsconcatrev  43337  rfovcnvfvd  43996  fsovrfovd  43998  dfafn5a  47109  sprsymrelfv  47418  sprsymrelfo  47421  upwlksfval  47978