Theorem opabbii 4056

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 4055	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

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

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 4051

This theorem is referenced by:  mptv  4086  fconstmpt  4658  xpundi  4667  xpundir  4668  inxp  4745  cnvco  4796  resopab  4935  opabresid  4944  cnvi  5015  cnvun  5016  cnvin  5018  cnvxp  5029  cnvcnv3  5060  coundi  5112  coundir  5113  mptun  5329  fvopab6  5592  cbvoprab1  5925  cbvoprab12  5927  dmoprabss  5935  mpomptx  5944  resoprab  5949  ov6g  5990  dfoprab3s  6169  dfoprab3  6170  dfoprab4  6171  mapsncnv  6673  xpcomco  6804  dmaddpq  7341  dmmulpq  7342  recmulnqg  7353  enq0enq  7393  ltrelxr  7980  ltxr  9732  shftidt2  10796  lmfval  12986  lmbr  13007  cnmptid  13075