Theorem opabbidv 5170

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811  {cab 2738  ⟨cop 4834  {copab 5166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-opab 5167

This theorem is used by:  opabbii  5171  mpteq12dva  5190  csbopab  5529  csbopabw  5530  csbmpt12  5531  xpeq1  5664  xpeq2  5671  opabbi2dv  5826  csbcnvgALTOLD  5865  resopab2  6027  mptcnv  6131  cores  6250  xpco  6292  dffn5  6943  f1oiso2  7360  fvmptopab  7475  f1ocnvd  7672  mpt3eqdv  7686  ofreq  7697  mptmpoopabbrd  8094  bropopvvv  8101  bropfvvvv  8103  f1od2  8110  fnwelem  8145  sprmpod  8244  mpocurryd  8289  cureq  8892  curf  8893  wemapwe  9701  ttrcleq  9713  xpcogend  15132  shftfval  15228  2shfti  15238  prdsval  17631  pwsle  17669  sectffval  17930  sectfval  17931  isfunc  18044  isfull  18092  isfth  18096  ipoval  18709  eqgfval  19393  eqg0subg  19416  dvdsrval  20596  dvdsrpropd  20651  ltbval  22357  opsrval  22360  lmfval  23555  xkocnv  24138  tgphaus  24441  isphtpc  25320  bcthlem1  25650  bcth  25655  dvcnp2  26245  dvmulbr  26264  dvcobr  26271  cmvth  26316  dvfsumle  26346  dvfsumlem2  26352  taylthlem2  26706  ulmval  26712  lgsquadlem3  27714  iscgrg  28980  legval  29052  ishlg2  29070  ishlg  29073  perpln1  29190  perpln2  29191  isperp  29192  ishpg  29242  iscgra  29321  tgaaddcpbllem2  29355  isinag  29362  isleag  29371  cgrabasimass  29383  brprlng  29421  wksfval  30195  upgrtrls  30289  upgrspthswlk  30329  ajfval  31416  f1o3d  33267  mgcoval  33593  inftmrel  33787  isinftm  33788  erlval  33865  rlocval  33866  quslsm  34002  idlsrgval  34081  metidval  34568  faeval  34925  eulerpartlemgvv  35054  eulerpart  35060  afsval  35349  onf1oracwevd  35971  satf  36204  satfvsuc  36212  satfv1  36214  satf0suc  36227  sat1el2xp  36230  fmlasuc0  36235  bj-imdirvallem  38194  bj-imdirval2  38197  bj-imdirco  38204  bj-iminvval2  38208  curunc  38618  fnopabeqd  38748  ecxrncnvep  39434  cosseq  39541  lcvfbr  40170  cmtfvalN  40360  cvrfval  40418  dicffval  42324  dicfval  42325  dicval  42326  prjspval  43724  prjspnerlem  43738  prjspnnorm  43754  0prjspn  43757  dnwech  44148  aomclem8  44156  tfsconcatun  44432  tfsconcat0i  44440  tfsconcatrev  44443  rfovcnvfvd  45100  fsovrfovd  45102  dfafn5a  48323  sprsymrelfv  48669  sprsymrelfo  48672  upwlksfval  49326  sectpropdlem  50243  upfval  50385  upfval2  50386  upfval3  50387  uppropd  50390