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

Theorem ifcli 4509
Description: Inference associated with ifcl 4507. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4519 when the special case 𝐵𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.)
Hypotheses
Ref Expression
ifcli.1 𝐴𝐶
ifcli.2 𝐵𝐶
Assertion
Ref Expression
ifcli if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem ifcli
StepHypRef Expression
1 ifcli.1 . 2 𝐴𝐶
2 ifcli.2 . 2 𝐵𝐶
3 ifcl 4507 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3mp2an 688 1 if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  ifcif 4463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-if 4464
This theorem is referenced by:  ifex  4511  xaddf  12605  sadcf  15790  ramcl  16353  setcepi  17336  abvtrivd  19540  mvrf1  20133  mplcoe3  20175  psrbagsn  20203  evlslem1  20223  marep01ma  21197  dscmet  23109  dscopn  23110  i1f1lem  24217  i1f1  24218  itg2const  24268  cxpval  25174  cxpcl  25184  recxpcl  25185  sqff1o  25686  chtublem  25714  dchrmulid2  25755  bposlem1  25787  lgsval  25804  lgsfcl2  25806  lgscllem  25807  lgsval2lem  25810  lgsneg  25824  lgsdilem  25827  lgsdir2  25833  lgsdir  25835  lgsdi  25837  lgsne0  25838  dchrisum0flblem1  26011  dchrisum0flblem2  26012  dchrisum0fno1  26014  rpvmasum2  26015  omlsi  29108  psgnfzto1stlem  30669  sgnsf  30731  indfval  31174  ddemeas  31394  eulerpartlemb  31525  eulerpartlemgs2  31537  ex-sategoelel12  32571  sqdivzi  32856  poimirlem16  34789  poimirlem19  34792  pw2f1ocnv  39512  flcidc  39652  arearect  39700  limsup10exlem  41929  sqwvfourb  42391  fouriersw  42393  hspval  42768
  Copyright terms: Public domain W3C validator