Theorem opabbidv 5152

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781  {cab 2715  ⟨cop 4574  {copab 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-opab 5149

This theorem is referenced by:  opabbii  5153  mpteq12dva  5172  csbopab  5503  csbopabgALT  5504  csbmpt12  5505  xpeq1  5638  xpeq2  5645  opabbi2dv  5798  csbcnvgALT  5833  resopab2  5995  mptcnv  6096  cores  6207  xpco  6247  dffn5  6892  f1oiso2  7300  fvmptopab  7415  f1ocnvd  7611  ofreq  7628  mptmpoopabbrd  8026  bropopvvv  8033  bropfvvvv  8035  fnwelem  8074  sprmpod  8167  mpocurryd  8212  wemapwe  9609  ttrcleq  9621  xpcogend  14927  shftfval  15023  2shfti  15033  prdsval  17409  pwsle  17447  sectffval  17708  sectfval  17709  isfunc  17822  isfull  17870  isfth  17874  ipoval  18487  eqgfval  19142  eqg0subg  19162  dvdsrval  20332  dvdsrpropd  20387  ltbval  22031  opsrval  22034  lmfval  23207  xkocnv  23789  tgphaus  24092  isphtpc  24971  bcthlem1  25301  bcth  25306  dvcnp2  25897  dvmulbr  25916  dvcobr  25923  cmvth  25968  dvfsumle  25998  dvfsumlem2  26004  taylthlem2  26351  ulmval  26358  lgsquadlem3  27359  iscgrg  28594  legval  28666  ishlg  28684  perpln1  28792  perpln2  28793  isperp  28794  ishpg  28841  iscgra  28891  isinag  28920  isleag  28929  wksfval  29693  upgrtrls  29783  upgrspthswlk  29821  ajfval  30895  f1o3d  32714  f1od2  32807  mgcoval  33061  inftmrel  33256  isinftm  33257  erlval  33334  rlocval  33335  quslsm  33480  idlsrgval  33578  metidval  34050  faeval  34406  eulerpartlemgvv  34536  eulerpart  34542  afsval  34831  satf  35551  satfvsuc  35559  satfv1  35561  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  bj-imdirvallem  37510  bj-imdirval2  37513  bj-imdirco  37520  bj-iminvval2  37524  cureq  37931  curf  37933  curunc  37937  fnopabeqd  38056  ecxrncnvep  38744  cosseq  38851  lcvfbr  39480  cmtfvalN  39670  cvrfval  39728  dicffval  41634  dicfval  41635  dicval  41636  prjspval  43050  prjspnerlem  43064  0prjspn  43075  dnwech  43494  aomclem8  43507  tfsconcatun  43783  tfsconcat0i  43791  tfsconcatrev  43794  rfovcnvfvd  44452  fsovrfovd  44454  dfafn5a  47620  sprsymrelfv  47966  sprsymrelfo  47969  upwlksfval  48623  sectpropdlem  49523  upfval  49663  upfval2  49664  upfval3  49665  uppropd  49668