Theorem opabbidv 5174

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-opab 5171

This theorem is used by:  opabbii  5175  mpteq12dva  5194  csbopab  5534  csbopabw  5535  csbmpt12  5536  xpeq1  5669  xpeq2  5676  opabbi2dv  5833  csbcnvgALTOLD  5873  resopab2  6040  mptcnv  6144  cores  6263  xpco  6310  dffn5  6966  f1oiso2  7383  fvmptopab  7498  f1ocnvd  7696  mpt3eqdv  7710  ofreq  7721  mptmpoopabbrd  8119  bropopvvv  8126  bropfvvvv  8128  f1od2  8135  fnwelem  8170  sprmpod  8269  mpocurryd  8314  cureq  8917  curf  8918  wemapwe  9725  ttrcleq  9737  xpcogend  15156  shftfval  15252  2shfti  15262  prdsval  17655  pwsle  17693  sectffval  17954  sectfval  17955  isfunc  18068  isfull  18116  isfth  18120  ipoval  18733  eqgfval  19417  eqg0subg  19440  dvdsrval  20621  dvdsrpropd  20676  ltbval  22382  opsrval  22385  lmfval  23580  xkocnv  24163  tgphaus  24466  isphtpc  25345  bcthlem1  25675  bcth  25680  dvcnp2  26270  dvmulbr  26289  dvcobr  26296  cmvth  26341  dvfsumle  26371  dvfsumlem2  26377  taylthlem2  26731  ulmval  26737  lgsquadlem3  27739  iscgrg  29005  legval  29077  ishlg2  29095  ishlg  29098  perpln1  29215  perpln2  29216  isperp  29217  ishpg  29267  iscgra  29346  tgaaddcpbllem2  29380  isinag  29387  isleag  29396  cgrabasimass  29408  brprlng  29446  wksfval  30220  upgrtrls  30314  upgrspthswlk  30354  ajfval  31441  f1o3d  33292  mgcoval  33617  inftmrel  33811  isinftm  33812  erlval  33889  rlocval  33890  quslsm  34026  idlsrgval  34105  metidval  34592  faeval  34949  eulerpartlemgvv  35078  eulerpart  35084  afsval  35373  onf1oracwevd  36052  satf  36285  satfvsuc  36293  satfv1  36295  satf0suc  36308  sat1el2xp  36311  fmlasuc0  36316  bj-imdirvallem  38293  bj-imdirval2  38296  bj-imdirco  38303  bj-iminvval2  38307  curunc  38717  fnopabeqd  38847  ecxrncnvep  39533  cosseq  39640  lcvfbr  40269  cmtfvalN  40459  cvrfval  40517  dicffval  42423  dicfval  42424  dicval  42425  prjspval  43824  prjspnerlem  43838  prjspnnorm  43854  0prjspn  43857  dnwech  44248  aomclem8  44256  tfsconcatun  44531  tfsconcat0i  44539  tfsconcatrev  44542  rfovcnvfvd  45199  fsovrfovd  45201  dfafn5a  48435  sprsymrelfv  48781  sprsymrelfo  48784  upwlksfval  49438  sectpropdlem  50355  upfval  50497  upfval2  50498  upfval3  50499  uppropd  50502