Theorem opabbidv 5218

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  ∃wex 1773  {cab 2702  ⟨cop 4638  {copab 5214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-opab 5215

This theorem is referenced by:  opabbii  5219  mpteq12dva  5241  csbopab  5560  csbopabgALT  5561  csbmpt12  5562  xpeq1  5695  xpeq2  5702  opabbi2dv  5855  csbcnvgALT  5890  resopab2  6044  mptcnv  6150  cores  6259  xpco  6299  dffn5  6960  f1oiso2  7363  fvmptopab  7478  fvmptopabOLD  7479  f1ocnvd  7676  ofreq  7693  mptmpoopabbrd  8093  mptmpoopabbrdOLD  8094  mptmpoopabbrdOLDOLD  8096  bropopvvv  8103  bropfvvvv  8105  fnwelem  8144  sprmpod  8238  mpocurryd  8283  wemapwe  9736  ttrcleq  9748  xpcogend  14974  shftfval  15070  2shfti  15080  prdsval  17465  pwsle  17502  sectffval  17761  sectfval  17762  isfunc  17878  isfull  17927  isfth  17931  ipoval  18550  eqgfval  19165  eqg0subg  19185  dvdsrval  20338  dvdsrpropd  20393  ltbval  22042  opsrval  22045  lmfval  23219  xkocnv  23801  tgphaus  24104  isphtpc  25003  bcthlem1  25335  bcth  25340  dvcnp2  25932  dvmulbr  25952  dvcobr  25960  cmvth  26006  dvfsumle  26037  dvfsumlem2  26044  taylthlem2  26394  ulmval  26401  lgsquadlem3  27403  iscgrg  28431  legval  28503  ishlg  28521  perpln1  28629  perpln2  28630  isperp  28631  ishpg  28678  iscgra  28728  isinag  28757  isleag  28766  wksfval  29538  upgrtrls  29630  upgrspthswlk  29667  ajfval  30734  f1o3d  32535  f1od2  32626  mgcoval  32844  inftmrel  33022  isinftm  33023  erlval  33090  rlocval  33091  quslsm  33257  idlsrgval  33355  metidval  33661  faeval  34035  eulerpartlemgvv  34166  eulerpart  34172  afsval  34473  satf  35133  satfvsuc  35141  satfv1  35143  satf0suc  35156  sat1el2xp  35159  fmlasuc0  35164  bj-imdirvallem  36835  bj-imdirval2  36838  bj-imdirco  36845  bj-iminvval2  36849  cureq  37245  curf  37247  curunc  37251  fnopabeqd  37370  cosseq  38072  lcvfbr  38666  cmtfvalN  38856  cvrfval  38914  dicffval  40821  dicfval  40822  dicval  40823  prjspval  42194  prjspnerlem  42208  0prjspn  42219  dnwech  42646  aomclem8  42659  tfsconcatun  42940  tfsconcat0i  42948  tfsconcatrev  42951  rfovcnvfvd  43611  fsovrfovd  43613  dfafn5a  46710  sprsymrelfv  47003  sprsymrelfo  47006  upwlksfval  47449