MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opabbii Structured version   Visualization version   GIF version

Theorem opabbii 4750
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 2651 . 2 𝑧 = 𝑧
2 opabbii.1 . . . 4 (𝜑𝜓)
32a1i 11 . . 3 (𝑧 = 𝑧 → (𝜑𝜓))
43opabbidv 4749 . 2 (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
51, 4ax-mp 5 1 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  {copab 4745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746
This theorem is referenced by:  mptv  4784  2rbropap  5046  dfid4  5055  fconstmpt  5197  xpundi  5205  xpundir  5206  inxp  5287  csbcnv  5338  cnvco  5340  resopab  5481  opabresid  5490  cnvi  5572  cnvun  5573  cnvxp  5586  cnvcnv3  5617  coundi  5674  coundir  5675  mptun  6063  fvopab6  6350  fmptsng  6475  fmptsnd  6476  cbvoprab1  6769  cbvoprab12  6771  dmoprabss  6784  mpt2mptx  6793  resoprab  6798  elrnmpt2res  6816  ov6g  6840  1st2val  7238  2nd2val  7239  dfoprab3s  7267  dfoprab3  7268  dfoprab4  7269  opabn1stprc  7272  mptmpt2opabbrd  7293  fsplit  7327  mapsncnv  7946  xpcomco  8091  marypha2lem2  8383  oemapso  8617  leweon  8872  r0weon  8873  compsscnv  9231  fpwwe  9506  ltrelxr  10137  ltxrlt  10146  ltxr  11987  shftidt2  13865  prdsle  16169  prdsless  16170  prdsleval  16184  dfiso2  16479  joindm  17050  meetdm  17064  gaorb  17786  efgcpbllema  18213  frgpuplem  18231  ltbval  19519  ltbwe  19520  opsrle  19523  opsrtoslem1  19532  opsrtoslem2  19533  dvdsrzring  19879  pjfval2  20101  lmfval  21084  lmbr  21110  cnmptid  21512  lgsquadlem3  25152  perpln1  25650  outpasch  25692  ishpg  25696  axcontlem2  25890  wksfval  26561  wlkson  26608  pthsfval  26673  ispth  26675  dfadj2  28872  dmadjss  28874  cnvadj  28879  mpt2mptxf  29605  fneer  32473  bj-dfmpt2a  33196  bj-mpt2mptALT  33197  opropabco  33648  cnvepres  34207  inxp2  34269  xrninxp  34290  xrninxp2  34291  rnxrnres  34297  rnxrncnvepres  34298  rnxrnidres  34299  dfcoss2  34311  dfcoss3  34312  1cossres  34324  dfcoels  34325  br1cosscnvxrn  34364  1cosscnvxrn  34365  coss0  34369  cossid  34370  dfssr2  34389  cmtfvalN  34815  cmtvalN  34816  cvrfval  34873  cvrval  34874  dicval2  36785  fgraphopab  38105  fgraphxp  38106  dfnelbr2  41614  opabbrfex0d  41628  opabbrfexd  41630  upwlksfval  42041  xpsnopab  42090  mpt2mptx2  42438
  Copyright terms: Public domain W3C validator