Theorem opabbidv 4198

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

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  {copab 4192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-opab 4194

This theorem is used by:  opabbii  4199  csbopabg  4210  xpeq1  4790  xpeq2  4791  opabbi2dv  4931  csbcnvg  4966  resopab2  5113  mptcnv  5193  cores  5294  xpcom  5337  dffn5im  5751  f1oiso2  6036  f1ocnvd  6295  f1o3d  6301  ofreq  6309  f1od2  6475  shftfvalg  11606  shftfval  11609  2shfti  11619  releqgg  14083  eqgex  14084  eqgfval  14085  prdsex  14280  prdsval  14281  dvdsrvald  14510  dvdsrpropdg  14564  aprval  14701  aprap  14708  aprprop  14711  lmfval  15431  lgsquadlem3  16415  wksfval  16780  trlsfvalg  16841  eupthsg  16903