Theorem opabbii 4070

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 2177	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 9	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 4069	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 105   = wceq 1353  {copab 4063

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-opab 4065

This theorem is referenced by:  mptv  4100  fconstmpt  4673  xpundi  4682  xpundir  4683  inxp  4761  cnvco  4812  resopab  4951  opabresid  4960  cnvi  5033  cnvun  5034  cnvin  5036  cnvxp  5047  cnvcnv3  5078  coundi  5130  coundir  5131  mptun  5347  fvopab6  5612  cbvoprab1  5946  cbvoprab12  5948  dmoprabss  5956  mpomptx  5965  resoprab  5970  ov6g  6011  dfoprab3s  6190  dfoprab3  6191  dfoprab4  6192  mapsncnv  6694  xpcomco  6825  dmaddpq  7377  dmmulpq  7378  recmulnqg  7389  enq0enq  7429  ltrelxr  8017  ltxr  9774  shftidt2  10840  prdsex  12717  releqgg  13078  dvdsrzring  13463  lmfval  13662  lmbr  13683  cnmptid  13751