Theorem opabbii 4054

Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)

Hypothesis

Ref	Expression
opabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem opabbii

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2170	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 9	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 4053	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 104   = wceq 1348  {copab 4047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-opab 4049

This theorem is referenced by:  mptv  4084  fconstmpt  4656  xpundi  4665  xpundir  4666  inxp  4743  cnvco  4794  resopab  4933  opabresid  4942  cnvi  5013  cnvun  5014  cnvin  5016  cnvxp  5027  cnvcnv3  5058  coundi  5110  coundir  5111  mptun  5327  fvopab6  5590  cbvoprab1  5923  cbvoprab12  5925  dmoprabss  5933  mpomptx  5942  resoprab  5947  ov6g  5988  dfoprab3s  6167  dfoprab3  6168  dfoprab4  6169  mapsncnv  6670  xpcomco  6801  dmaddpq  7330  dmmulpq  7331  recmulnqg  7342  enq0enq  7382  ltrelxr  7969  ltxr  9721  shftidt2  10785  lmfval  12947  lmbr  12968  cnmptid  13036