ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opabbii GIF version

Theorem opabbii 3865
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.
StepHypRef Expression
1 eqid 2083 . 2 𝑧 = 𝑧
2 opabbii.1 . . . 4 (𝜑𝜓)
32a1i 9 . . 3 (𝑧 = 𝑧 → (𝜑𝜓))
43opabbidv 3864 . 2 (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
51, 4ax-mp 7 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1285  {copab 3858
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-opab 3860
This theorem is referenced by:  mptv  3894  fconstmpt  4433  xpundi  4442  xpundir  4443  inxp  4518  cnvco  4568  resopab  4702  opabresid  4709  cnvi  4778  cnvun  4779  cnvin  4781  cnvxp  4792  cnvcnv3  4820  coundi  4872  coundir  4873  mptun  5080  fvopab6  5317  cbvoprab1  5628  cbvoprab12  5630  dmoprabss  5638  mpt2mptx  5647  resoprab  5649  ov6g  5690  dfoprab3s  5868  dfoprab3  5869  dfoprab4  5870  xpcomco  6392  dmaddpq  6701  dmmulpq  6702  recmulnqg  6713  enq0enq  6753  ltrelxr  7310  ltxr  8997  shftidt2  9939
  Copyright terms: Public domain W3C validator