Theorem opabbidv 5105

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787  {cab 2714  ⟨cop 4533  {copab 5101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-opab 5102

This theorem is referenced by:  opabbii  5106  csbopab  5421  csbopabgALT  5422  csbmpt12  5423  xpeq1  5550  xpeq2  5557  opabbi2dv  5703  csbcnvgALT  5738  resopab2  5889  mptcnv  5983  cores  6093  xpco  6132  dffn5  6749  f1oiso2  7139  fvmptopab  7244  f1ocnvd  7434  ofreq  7450  mptmpoopabbrd  7829  bropopvvv  7836  bropfvvvv  7838  fnwelem  7876  sprmpod  7944  mpocurryd  7989  wemapwe  9290  xpcogend  14502  shftfval  14598  2shfti  14608  prdsval  16914  pwsle  16951  sectffval  17209  sectfval  17210  isfunc  17324  isfull  17371  isfth  17375  ipoval  17990  eqgfval  18546  dvdsrval  19617  dvdsrpropd  19668  ltbval  20954  opsrval  20957  lmfval  22083  xkocnv  22665  tgphaus  22968  isphtpc  23845  bcthlem1  24175  bcth  24180  ulmval  25226  lgsquadlem3  26217  iscgrg  26557  legval  26629  ishlg  26647  perpln1  26755  perpln2  26756  isperp  26757  ishpg  26804  iscgra  26854  isinag  26883  isleag  26892  wksfval  27651  upgrtrls  27743  upgrspthswlk  27779  ajfval  28844  f1o3d  30635  f1od2  30730  mgcoval  30937  inftmrel  31107  isinftm  31108  quslsm  31261  idlsrgval  31316  metidval  31508  faeval  31880  eulerpartlemgvv  32009  eulerpart  32015  afsval  32317  satf  32982  satfvsuc  32990  satfv1  32992  satf0suc  33005  sat1el2xp  33008  fmlasuc0  33013  bj-imdirvallem  35035  bj-imdirval2  35038  bj-imdirco  35045  bj-iminvval2  35049  cureq  35439  curf  35441  curunc  35445  fnopabeqd  35564  cosseq  36235  lcvfbr  36720  cmtfvalN  36910  cvrfval  36968  dicffval  38874  dicfval  38875  dicval  38876  prjspval  40091  prjspnerlem  40105  0prjspn  40114  dnwech  40517  aomclem8  40530  rfovcnvfvd  41233  fsovrfovd  41235  dfafn5a  44267  sprsymrelfv  44562  sprsymrelfo  44565  upwlksfval  44913