Theorem opabbidv 4155

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 4154	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-opab 4151

This theorem is referenced by:  opabbii  4156  csbopabg  4167  xpeq1  4739  xpeq2  4740  opabbi2dv  4879  csbcnvg  4914  resopab2  5060  mptcnv  5139  cores  5240  xpcom  5283  dffn5im  5691  f1oiso2  5968  f1ocnvd  6225  ofreq  6239  f1od2  6400  shftfvalg  11380  shftfval  11383  2shfti  11393  prdsex  13354  prdsval  13358  releqgg  13809  eqgex  13810  eqgfval  13811  dvdsrvald  14110  dvdsrpropdg  14164  aprval  14299  aprap  14303  lmfval  14920  lgsquadlem3  15811  wksfval  16176  trlsfvalg  16237  eupthsg  16299