Theorem opabbidv 5161

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  {cab 2707  ⟨cop 4585  {copab 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-opab 5158

This theorem is referenced by:  opabbii  5162  mpteq12dva  5181  csbopab  5502  csbopabgALT  5503  csbmpt12  5504  xpeq1  5637  xpeq2  5644  opabbi2dv  5796  csbcnvgALT  5831  resopab2  5991  mptcnv  6092  cores  6202  xpco  6241  dffn5  6885  f1oiso2  7293  fvmptopab  7408  f1ocnvd  7604  ofreq  7621  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  bropopvvv  8030  bropfvvvv  8032  fnwelem  8071  sprmpod  8164  mpocurryd  8209  wemapwe  9612  ttrcleq  9624  xpcogend  14899  shftfval  14995  2shfti  15005  prdsval  17377  pwsle  17414  sectffval  17675  sectfval  17676  isfunc  17789  isfull  17837  isfth  17841  ipoval  18454  eqgfval  19073  eqg0subg  19093  dvdsrval  20264  dvdsrpropd  20319  ltbval  21966  opsrval  21969  lmfval  23135  xkocnv  23717  tgphaus  24020  isphtpc  24909  bcthlem1  25240  bcth  25245  dvcnp2  25837  dvmulbr  25857  dvcobr  25865  cmvth  25911  dvfsumle  25942  dvfsumlem2  25949  taylthlem2  26298  ulmval  26305  lgsquadlem3  27309  iscgrg  28475  legval  28547  ishlg  28565  perpln1  28673  perpln2  28674  isperp  28675  ishpg  28722  iscgra  28772  isinag  28801  isleag  28810  wksfval  29573  upgrtrls  29663  upgrspthswlk  29701  ajfval  30771  f1o3d  32584  f1od2  32677  mgcoval  32941  inftmrel  33132  isinftm  33133  erlval  33208  rlocval  33209  quslsm  33352  idlsrgval  33450  metidval  33856  faeval  34212  eulerpartlemgvv  34343  eulerpart  34349  afsval  34638  satf  35325  satfvsuc  35333  satfv1  35335  satf0suc  35348  sat1el2xp  35351  fmlasuc0  35356  bj-imdirvallem  37153  bj-imdirval2  37156  bj-imdirco  37163  bj-iminvval2  37167  cureq  37575  curf  37577  curunc  37581  fnopabeqd  37700  cosseq  38402  lcvfbr  38998  cmtfvalN  39188  cvrfval  39246  dicffval  41153  dicfval  41154  dicval  41155  prjspval  42576  prjspnerlem  42590  0prjspn  42601  dnwech  43021  aomclem8  43034  tfsconcatun  43310  tfsconcat0i  43318  tfsconcatrev  43321  rfovcnvfvd  43980  fsovrfovd  43982  dfafn5a  47145  sprsymrelfv  47479  sprsymrelfo  47482  upwlksfval  48120  sectpropdlem  49022  upfval  49162  upfval2  49163  upfval3  49164  uppropd  49167