Theorem oprabbii 6076

Description: Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Hypothesis

Ref	Expression
oprabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
oprabbii	⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)

Proof of Theorem oprabbii

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2231	. 2 ⊢ 𝑤 = 𝑤
2		oprabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 9	. . 3 ⊢ (𝑤 = 𝑤 → (𝜑 ↔ 𝜓))
4	3	oprabbidv 6075	. 2 ⊢ (𝑤 = 𝑤 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 105   = wceq 1397  {coprab 6019

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-oprab 6022

This theorem is referenced by:  oprab4  6092  mpov  6111  dfxp3  6359  tposmpo  6447  oviec  6810  dfplpq2  7574  dfmpq2  7575  dfmq0qs  7649  dfplq0qs  7650  addsrpr  7965  mulsrpr  7966  addcnsr  8054  mulcnsr  8055  addvalex  8064