Theorem opabbii 4177

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

Syntax hints:   ↔ wb 105   = wceq 1398  {copab 4170

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-opab 4172

This theorem is referenced by:  mptv  4207  fconstmpt  4797  xpundi  4806  xpundir  4807  inxp  4889  cnvco  4940  resopab  5082  opabresid  5091  cnvi  5167  cnvun  5168  cnvin  5170  cnvxp  5181  cnvcnv3  5212  coundi  5264  coundir  5265  mptun  5490  fvopab6  5774  cbvoprab1  6125  cbvoprab12  6127  dmoprabss  6135  mpomptx  6144  resoprab  6149  ov6g  6192  dfoprab3s  6384  dfoprab3  6385  dfoprab4  6386  opabn1stprc  6389  mapsncnv  6930  xpcomco  7077  dmaddpq  7694  dmmulpq  7695  recmulnqg  7706  enq0enq  7746  ltrelxr  8334  ltxr  10108  shftidt2  11517  prdsex  13482  prdsval  13486  prdsbaslemss  13487  releqgg  13937  eqgex  13938  dvdsrzring  14751  lmfval  15058  lmbr  15078  cnmptid  15146  lgsquadlem3  15952  wksfval  16317