Theorem opabbidv 4129

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375  {copab 4123

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-opab 4125

This theorem is referenced by:  opabbii  4130  csbopabg  4141  xpeq1  4710  xpeq2  4711  opabbi2dv  4848  csbcnvg  4883  resopab2  5028  mptcnv  5107  cores  5208  xpcom  5251  dffn5im  5652  f1oiso2  5924  f1ocnvd  6178  ofreq  6192  f1od2  6351  shftfvalg  11295  shftfval  11298  2shfti  11308  prdsex  13268  prdsval  13272  releqgg  13723  eqgex  13724  eqgfval  13725  reldvdsrsrg  14021  dvdsrvald  14022  dvdsrpropdg  14076  aprval  14211  aprap  14215  lmfval  14831  lgsquadlem3  15723