Theorem opabbidv 4156

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 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1576	. 2 ⊢ Ⅎ𝑦𝜑
3		opabbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 2, 3	opabbid 4155	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  {copab 4150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-opab 4152

This theorem is referenced by:  opabbii  4157  csbopabg  4168  xpeq1  4741  xpeq2  4742  opabbi2dv  4881  csbcnvg  4916  resopab2  5062  mptcnv  5141  cores  5242  xpcom  5285  dffn5im  5694  f1oiso2  5973  f1ocnvd  6230  ofreq  6244  f1od2  6405  shftfvalg  11401  shftfval  11404  2shfti  11414  prdsex  13375  prdsval  13379  releqgg  13830  eqgex  13831  eqgfval  13832  dvdsrvald  14131  dvdsrpropdg  14185  aprval  14320  aprap  14324  lmfval  14946  lgsquadlem3  15837  wksfval  16202  trlsfvalg  16263  eupthsg  16325