Theorem ifcl 2378

Description: Membership (closure) of a conditional operator.

Assertion

Ref	Expression
ifcl	|- ((A e. C /\ B e. C) -> if(ph, A, B) e. C)

Proof of Theorem ifcl

Step	Hyp	Ref	Expression
1		eleq1 1533	. 2 |- (A = if(ph, A, B) -> (A e. C <-> if(ph, A, B) e. C))
2		eleq1 1533	. 2 |- (B = if(ph, A, B) -> (B e. C <-> if(ph, A, B) e. C))
3	1, 2	ifboth 2373	1 |- ((A e. C /\ B e. C) -> if(ph, A, B) e. C)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 957  ifcif 2359

This theorem is referenced by:  ifpr 2425  suppr 4577  xrmaxltt 5875  xrltmint 5876  maxlet 5880  lemint 5883  maxltt 5884  z2get 6149  iooint 6327  fsequb 6473  seq1bnd 6876  caubnd 6892  clm3 7047  ivthlem7 7258  ivthlem7OLD 7267  retopbas 7634  xpcn 7959  iscms2lem4 7975  spwval2 8636

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2360

Copyright terms: Public domain