Theorem opabbidv 4642

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (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

Step	Hyp	Ref	Expression
1		nfv 1829	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1829	. 2 ⊢ Ⅎ𝑦𝜑
3		opabbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 2, 3	opabbid 4641	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 194   = wceq 1474  {copab 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-opab 4638

This theorem is referenced by:  opabbii  4643  csbopab  4922  csbopabgALT  4923  csbmpt12  4924  xpeq1  5042  xpeq2  5043  opabbi2dv  5181  csbcnvgALT  5217  resopab2  5355  mptcnv  5440  cores  5541  xpco  5578  dffn5  6136  f1oiso2  6480  fvmptopab1  6572  f1ocnvd  6760  ofreq  6776  bropopvvv  7120  bropfvvvv  7122  fnwelem  7157  sprmpt2d  7215  mpt2curryd  7260  wemapwe  8455  xpcogend  13510  shftfval  13607  2shfti  13617  prdsval  15887  pwsle  15924  sectffval  16182  sectfval  16183  isfunc  16296  isfull  16342  isfth  16346  ipoval  16926  eqgfval  17414  dvdsrval  18417  dvdsrpropd  18468  ltbval  19241  opsrval  19244  lmfval  20794  xkocnv  21375  tgphaus  21678  isphtpc  22549  bcthlem1  22874  bcth  22879  ulmval  23883  lgsquadlem3  24852  iscgrg  25153  legval  25225  ishlg  25243  perpln1  25351  perpln2  25352  isperp  25353  ishpg  25397  iscgra  25447  isinag  25475  isleag  25479  wlks  25841  wlkcompim  25848  wlkelwrd  25852  wlkon  25855  trls  25860  trlon  25864  pths  25890  spths  25891  pthon  25899  spthon  25906  clwlk  26075  clwlkcompim  26086  iseupa  26286  ajfval  26882  f1o3d  28647  f1od2  28721  inftmrel  28899  isinftm  28900  metidval  29095  faeval  29470  eulerpartlemgvv  29599  eulerpart  29605  afsval  29836  cureq  32379  curf  32381  curunc  32385  fnopabeqd  32508  lcvfbr  33149  cmtfvalN  33339  cvrfval  33397  dicffval  35305  dicfval  35306  dicval  35307  dnwech  36460  aomclem8  36473  rfovcnvfvd  37145  fsovrfovd  37147  dfafn5a  39714  mptmpt2opabbrd  40182  1wlksfval  40833  wlksfval  40834  upgrtrls  40931  upgrspths1wlk  40966